ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)<VAR>x : (CategoryTheory.Pairwise ι)ᵒᵖ<GOAL>((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).obj c).π.app x = CategoryTheory.Pairwise.rec (fun a => CategoryTheory.Limits.Fork.ι c ≫ CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op (U i))) a) (fun a a_1 => CategoryTheory.Limits.Fork.ι c ≫ TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U ≫ CategoryTheory.Limits.Pi.π (fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1)) (Opposite.unop x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp F U c).hom.hom = 𝟙 ((𝟭 (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F))).obj c).pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp F U c).inv.hom = 𝟙 ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U ⋙ TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).obj c).pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>∀ (X_1 : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)), ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U).inv.app X_1).hom = 𝟙 X_1.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>∀ (X_1 : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)), ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U).hom.app X_1).hom = 𝟙 X_1.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>∀ (X_1 : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)), ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U).inv.app X_1).hom = 𝟙 X_1.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>∀ (X_1 : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)), ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U).hom.app X_1).hom = 𝟙 X_1.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).functor = TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).unitIso = TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).counitIso = TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).inverse = TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheaf ↔ F.IsSheafEqualizerProducts
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>TopologicalSpace K<VAR>ContinuousMul K<VAR>a : K<VAR>ha : a ≠ 0<GOAL>Filter.Tendsto (fun x => a * x) (Filter.cocompact K) (Filter.cocompact K)
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>TopologicalSpace K<VAR>ContinuousMul K<VAR>a : K<VAR>ha : a ≠ 0<GOAL>Filter.Tendsto (fun x => x * a) (Filter.cocompact K) (Filter.cocompact K)
<VAR>α : Type u_2<VAR>Field α<VAR>TopologicalSpace α<VAR>TopologicalDivisionRing α<VAR>s : Subfield α<GOAL>s ≤ s.topologicalClosure
<VAR>α : Type u_2<VAR>Field α<VAR>TopologicalSpace α<VAR>TopologicalDivisionRing α<VAR>s : Subfield α<GOAL>IsClosed ↑s.topologicalClosure
<VAR>α : Type u_2<VAR>Field α<VAR>TopologicalSpace α<VAR>TopologicalDivisionRing α<VAR>s : Subfield α<VAR>t : Subfield α<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>a b : 𝕜<VAR>h : a ≠ 0<VAR>y : 𝕜<GOAL>(affineHomeomorph a b h).symm y = (y - b) / a
<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>a b : 𝕜<VAR>h : a ≠ 0<VAR>x : 𝕜<GOAL>(affineHomeomorph a b h) x = a * x + b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrderedSemifield β<VAR>f : α → β<VAR>a : α<VAR>h1 : IsLocalMin f a<VAR>h2 : ∀ᶠ (z : α) in nhds a, 0 < f z<GOAL>IsLocalMax f⁻¹ a
<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f : α → 𝕜<VAR>S : Set α<VAR>TopologicalSpace α<VAR>TopologicalSpace 𝕜<VAR>T1Space 𝕜<VAR>Ring 𝕜<VAR>NoZeroDivisors 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hsq : Set.EqOn (f ^ 2) 1 S<GOAL>Set.EqOn f 1 S ∨ Set.EqOn f (-1) S
<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>TopologicalSpace α<VAR>TopologicalSpace 𝕜<VAR>T1Space 𝕜<VAR>Field 𝕜<VAR>HasContinuousInv₀ 𝕜<VAR>ContinuousMul 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hg : ContinuousOn g S<VAR>hsq : Set.EqOn (f ^ 2) (g ^ 2) S<VAR>hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0<GOAL>Set.EqOn f g S ∨ Set.EqOn f (-g) S
<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>TopologicalSpace α<VAR>TopologicalSpace 𝕜<VAR>T1Space 𝕜<VAR>Field 𝕜<VAR>HasContinuousInv₀ 𝕜<VAR>ContinuousMul 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hg : ContinuousOn g S<VAR>hsq : Set.EqOn (f ^ 2) (g ^ 2) S<VAR>hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0<VAR>y : α<VAR>hy : y ∈ S<VAR>hy' : f y = g y<GOAL>Set.EqOn f g S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Monoid γ<VAR>TopologicalSpace α<VAR>AddCommMonoid α<VAR>DistribMulAction γ α<VAR>ContinuousConstSMul γ α<VAR>f : β → α<VAR>a : α<VAR>b : γ<VAR>hf : HasSum f a<GOAL>HasSum (fun i => b • f i) (b • a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Monoid γ<VAR>TopologicalSpace α<VAR>AddCommMonoid α<VAR>DistribMulAction γ α<VAR>ContinuousConstSMul γ α<VAR>f : β → α<VAR>b : γ<VAR>hf : Summable f<GOAL>Summable fun i => b • f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Monoid γ<VAR>TopologicalSpace α<VAR>AddCommMonoid α<VAR>DistribMulAction γ α<VAR>ContinuousConstSMul γ α<VAR>f : β → α<VAR>T2Space α<VAR>b : γ<VAR>hf : Summable f<GOAL>∑' (i : β), b • f i = b • ∑' (i : β), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>AddCommMonoid α<VAR>f : β → α<VAR>γ : Type u_5<VAR>Group γ<VAR>DistribMulAction γ α<VAR>ContinuousConstSMul γ α<VAR>T2Space α<VAR>g : γ<GOAL>∑' (i : β), g • f i = g • ∑' (i : β), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>AddCommMonoid α<VAR>f : β → α<VAR>γ : Type u_5<VAR>DivisionRing γ<VAR>Module γ α<VAR>ContinuousConstSMul γ α<VAR>T2Space α<VAR>g : γ<GOAL>∑' (i : β), g • f i = g • ∑' (i : β), f i
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>M : Type u_9<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousSMul R M<VAR>f : ι → R<VAR>r : R<VAR>hf : HasSum f r<VAR>a : M<GOAL>HasSum (fun z => f z • a) (r • a)
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>M : Type u_9<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousSMul R M<VAR>f : ι → R<VAR>hf : Summable f<VAR>a : M<GOAL>Summable fun z => f z • a
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>M : Type u_9<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousSMul R M<VAR>f : ι → R<VAR>T2Space M<VAR>hf : Summable f<VAR>a : M<GOAL>∑' (z : ι), f z • a = (∑' (z : ι), f z) • a
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R : Type u_7<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>T3Space M<VAR>ContinuousAdd M<VAR>ContinuousSMul R M<VAR>f : ι → R<VAR>g : κ → M<VAR>s : R<VAR>t u : M<VAR>hf : HasSum f s<VAR>hg : HasSum g t<VAR>hfg : HasSum (fun x => f x.1 • g x.2) u<GOAL>s • t = u
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R : Type u_7<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>T3Space M<VAR>ContinuousAdd M<VAR>ContinuousSMul R M<VAR>f : ι → R<VAR>g : κ → M<VAR>s : R<VAR>t : M<VAR>hf : HasSum f s<VAR>hg : HasSum g t<VAR>hfg : Summable fun x => f x.1 • g x.2<GOAL>HasSum (fun x => f x.1 • g x.2) (s • t)
<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R : Type u_7<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>T3Space M<VAR>ContinuousAdd M<VAR>ContinuousSMul R M<VAR>f : ι → R<VAR>g : κ → M<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 • g x.2<GOAL>(∑' (x : ι), f x) • ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 • g z.2
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>f : ι → M<VAR>φ : M →SL[σ] M₂<VAR>x : M<VAR>hf : HasSum f x<GOAL>HasSum (fun b => φ (f b)) (φ x)
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>f : ι → M<VAR>φ : M →SL[σ] M₂<VAR>hf : Summable f<GOAL>Summable fun b => φ (f b)
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>T2Space M₂<VAR>f : ι → M<VAR>φ : M →SL[σ] M₂<VAR>hf : Summable f<GOAL>φ (∑' (z : ι), f z) = ∑' (z : ι), φ (f z)
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<VAR>y : M₂<GOAL>HasSum (fun b => e (f b)) y ↔ HasSum f (e.symm y)
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<VAR>x : M<GOAL>HasSum (fun b => e (f b)) (e x) ↔ HasSum f x
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<GOAL>(Summable fun b => e (f b)) ↔ Summable f
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>T2Space M<VAR>T2Space M₂<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<VAR>y : M₂<GOAL>∑' (z : ι), e (f z) = y ↔ ∑' (z : ι), f z = e.symm y
<VAR>ι : Type u_5<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>T2Space M<VAR>T2Space M₂<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<GOAL>e (∑' (z : ι), f z) = ∑' (z : ι), e (f z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_11<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>T2Space M<VAR>R : Type u_12<VAR>DivisionRing R<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>Group α<VAR>MulAction α β<VAR>f : β → M<VAR>g : Quotient (MulAction.orbitRel α β) → R<GOAL>MulAction.automorphize (g ∘ Quotient.mk' • f) = g • MulAction.automorphize f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_11<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>T2Space M<VAR>R : Type u_12<VAR>DivisionRing R<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>AddGroup α<VAR>AddAction α β<VAR>f : β → M<VAR>g : Quotient (AddAction.orbitRel α β) → R<GOAL>AddAction.automorphize (g ∘ Quotient.mk' • f) = g • AddAction.automorphize f
<VAR>M : Type u_11<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>T2Space M<VAR>R : Type u_12<VAR>DivisionRing R<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>G : Type u_13<VAR>Group G<VAR>Γ : Subgroup G<VAR>f : G → M<VAR>g : G ⧸ Γ → R<GOAL>QuotientGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientGroup.automorphize f
<VAR>M : Type u_11<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>T2Space M<VAR>R : Type u_12<VAR>DivisionRing R<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>G : Type u_13<VAR>AddGroup G<VAR>Γ : AddSubgroup G<VAR>f : G → M<VAR>g : G ⧸ Γ → R<GOAL>QuotientAddGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientAddGroup.automorphize f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>self : BoundedContinuousFunction α β<GOAL>∃ C, ∀ (x y : α), dist (self.toFun x) (self.toFun y) ≤ C
<VAR>F : Type u_2<VAR>α : outParam (Type u_3)<VAR>β : outParam (Type u_4)<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>self : BoundedContinuousMapClass F α β<VAR>f : F<GOAL>∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f : BoundedContinuousFunction α β<GOAL>⇑f.toContinuousMap = ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f : BoundedContinuousFunction α β<GOAL>∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f : BoundedContinuousFunction α β<GOAL>Continuous ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f : BoundedContinuousFunction α β<GOAL>Bornology.IsBounded (Set.range ⇑f)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f : BoundedContinuousFunction α β<VAR>s : Set α<GOAL>Bornology.IsBounded (⇑f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>h : IsEmpty α<VAR>f g : BoundedContinuousFunction α β<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f : C(α, β)<VAR>C : ℝ<VAR>h : ∀ (x y : α), dist (f x) (f y) ≤ C<GOAL>⇑(BoundedContinuousFunction.mkOfBound f C h) = ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>CompactSpace α<VAR>f : C(α, β)<VAR>a : α<GOAL>(BoundedContinuousFunction.mkOfCompact f) a = f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>DiscreteTopology α<VAR>f : α → β<VAR>C : ℝ<VAR>h : ∀ (x y : α), dist (f x) (f y) ≤ C<GOAL>∀ (a : α), (BoundedContinuousFunction.mkOfDiscrete f C h) a = f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<GOAL>dist f g = sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<GOAL>∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>x : α<GOAL>dist (f x) (g x) ≤ dist f g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<GOAL>0 ≤ dist f g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>C : ℝ<VAR>C0 : 0 ≤ C<GOAL>dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>C : ℝ<VAR>Nonempty α<GOAL>dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>C : ℝ<VAR>Nonempty α<VAR>CompactSpace α<VAR>w : ∀ (x : α), dist (f x) (g x) < C<GOAL>dist f g < C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>C : ℝ<VAR>CompactSpace α<VAR>C0 : 0 < C<GOAL>dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>C : ℝ<VAR>Nonempty α<VAR>CompactSpace α<GOAL>dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<GOAL>nndist f g = sInf {C | ∀ (x : α), nndist (f x) (g x) ≤ C}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<GOAL>∃ C, ∀ (x : α), nndist (f x) (g x) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>x : α<GOAL>nndist (f x) (g x) ≤ nndist f g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<VAR>IsEmpty α<GOAL>dist f g = 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<GOAL>dist f g = ⨆ x, dist (f x) (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f g : BoundedContinuousFunction α β<GOAL>nndist f g = ⨆ x, nndist (f x) (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>ι : Type u_2<VAR>F : ι → BoundedContinuousFunction α β<VAR>f : BoundedContinuousFunction α β<VAR>l : Filter ι<GOAL>Filter.Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => ⇑(F i)) (⇑f) l
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<GOAL>Inducing (⇑UniformFun.ofFun ∘ DFunLike.coe)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<GOAL>Embedding (⇑UniformFun.ofFun ∘ DFunLike.coe)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>b : β<GOAL>⇑(BoundedContinuousFunction.const α b) = fun x => b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>a : α<VAR>b : β<GOAL>(BoundedContinuousFunction.const α b) a = b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>x : α<GOAL>LipschitzWith 1 fun f => f x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<GOAL>UniformContinuous DFunLike.coe
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<GOAL>Continuous fun f x => f x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>x : α<GOAL>Continuous fun f => f x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<GOAL>Continuous fun p => p.1 p.2
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>f : BoundedContinuousFunction α β<VAR>g : C(δ, α)<GOAL>⇑(f.compContinuous g) = ⇑f ∘ ⇑g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>f : BoundedContinuousFunction α β<VAR>g : C(δ, α)<VAR>x : δ<GOAL>(f.compContinuous g) x = f (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>g : C(δ, α)<GOAL>LipschitzWith 1 fun f => f.compContinuous g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>g : C(δ, α)<GOAL>Continuous fun f => f.compContinuous g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f : BoundedContinuousFunction α β<VAR>s : Set α<GOAL>⇑(f.restrict s) = ⇑f ∘ Subtype.val
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>f : BoundedContinuousFunction α β<VAR>s : Set α<VAR>x : ↑s<GOAL>(f.restrict s) x = f ↑x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>PseudoMetricSpace γ<VAR>G : β → γ<VAR>C : ℝ≥0<VAR>H : LipschitzWith C G<GOAL>LipschitzWith C (BoundedContinuousFunction.comp G H)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>PseudoMetricSpace γ<VAR>G : β → γ<VAR>C : ℝ≥0<VAR>H : LipschitzWith C G<GOAL>UniformContinuous (BoundedContinuousFunction.comp G H)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>PseudoMetricSpace γ<VAR>G : β → γ<VAR>C : ℝ≥0<VAR>H : LipschitzWith C G<GOAL>Continuous (BoundedContinuousFunction.comp G H)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>DiscreteTopology δ<VAR>f : α ↪ δ<VAR>g : BoundedContinuousFunction α β<VAR>h : BoundedContinuousFunction δ β<VAR>x : α<GOAL>(BoundedContinuousFunction.extend f g h) (f x) = g x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>DiscreteTopology δ<VAR>f : α ↪ δ<VAR>g : BoundedContinuousFunction α β<VAR>h : BoundedContinuousFunction δ β<GOAL>⇑(BoundedContinuousFunction.extend f g h) ∘ ⇑f = ⇑g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>DiscreteTopology δ<VAR>f : α ↪ δ<VAR>x : δ<VAR>hx : x ∉ Set.range ⇑f<VAR>g : BoundedContinuousFunction α β<VAR>h : BoundedContinuousFunction δ β<GOAL>(BoundedContinuousFunction.extend f g h) x = h x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>DiscreteTopology δ<VAR>IsEmpty α<VAR>f : α ↪ δ<VAR>g : BoundedContinuousFunction α β<VAR>h : BoundedContinuousFunction δ β<GOAL>BoundedContinuousFunction.extend f g h = h