ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>f g : A →A[R] A<GOAL>f * g = f.comp g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>f g : A →A[R] A<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>f g : A →A[R] A<VAR>x : A<GOAL>(f * g) x = f (g x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>f : A →A[R] A<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>f : A →A[R] A<GOAL>ContinuousAlgHom.toAlgHomMonoidHom f = ↑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>f₁ : A →A[R] B<VAR>f₂ : A →A[R] C<GOAL>↑(f₁.prod f₂) = (↑f₁).prod ↑f₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>f₁ : A →A[R] B<VAR>f₂ : A →A[R] C<VAR>x : A<GOAL>(f₁.prod f₂) x = (f₁ x, f₂ x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<GOAL>↑(ContinuousAlgHom.fst R A B) = AlgHom.fst R A B
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<GOAL>⇑(ContinuousAlgHom.fst R A B) = Prod.fst
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<GOAL>↑(ContinuousAlgHom.snd R A B) = AlgHom.snd R A B
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<GOAL>⇑(ContinuousAlgHom.snd R A B) = Prod.snd
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<GOAL>(ContinuousAlgHom.fst R A B).prod (ContinuousAlgHom.snd R A B) = ContinuousAlgHom.id R (A × B)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>f : A →A[R] B<VAR>g : A →A[R] C<GOAL>(ContinuousAlgHom.fst R B C).comp (f.prod g) = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>f : A →A[R] B<VAR>g : A →A[R] C<GOAL>(ContinuousAlgHom.snd R B C).comp (f.prod g) = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>D : Type u_6<VAR>Semiring D<VAR>TopologicalSpace D<VAR>Algebra R D<VAR>f₁ : A →A[R] B<VAR>f₂ : C →A[R] D<GOAL>↑(f₁.prodMap f₂) = (↑f₁).prodMap ↑f₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>D : Type u_6<VAR>Semiring D<VAR>TopologicalSpace D<VAR>Algebra R D<VAR>f₁ : A →A[R] B<VAR>f₂ : C →A[R] D<GOAL>⇑(f₁.prodMap f₂) = Prod.map ⇑f₁ ⇑f₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>f : (A →A[R] B) × (A →A[R] C)<GOAL>ContinuousAlgHom.prodEquiv f = f.1.prod f.2
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<VAR>p : Subalgebra R B<VAR>h : ∀ (x : A), f x ∈ p<GOAL>↑(f.codRestrict p h) = (↑f).codRestrict p h
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<VAR>p : Subalgebra R B<VAR>h : ∀ (x : A), f x ∈ p<VAR>x : A<GOAL>↑((f.codRestrict p h) x) = f x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<GOAL>↑f.rangeRestrict = (↑f).rangeRestrict
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>p : Subalgebra R A<GOAL>↑↑p.valA = p.subtype
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>p : Subalgebra R A<GOAL>⇑p.valA = ⇑p.subtype
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>p : Subalgebra R A<VAR>x : ↥p<GOAL>p.valA x = ↑x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>p : Subalgebra R A<GOAL>(↑p.valA).range = p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_3<VAR>Ring S<VAR>TopologicalSpace S<VAR>Algebra R S<VAR>B : Type u_4<VAR>Ring B<VAR>TopologicalSpace B<VAR>Algebra R B<VAR>f : S →A[R] B<VAR>x : S<GOAL>f (-x) = -f x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_3<VAR>Ring S<VAR>TopologicalSpace S<VAR>Algebra R S<VAR>B : Type u_4<VAR>Ring B<VAR>TopologicalSpace B<VAR>Algebra R B<VAR>f : S →A[R] B<VAR>x y : S<GOAL>f (x - y) = f x - f y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_3<VAR>CommSemiring S<VAR>Algebra R S<VAR>B : Type u_4<VAR>Ring B<VAR>TopologicalSpace B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>C : Type u_5<VAR>Ring C<VAR>TopologicalSpace C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>f : B →A[S] C<GOAL>↑(ContinuousAlgHom.restrictScalars R f) = AlgHom.restrictScalars R ↑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_3<VAR>CommSemiring S<VAR>Algebra R S<VAR>B : Type u_4<VAR>Ring B<VAR>TopologicalSpace B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>C : Type u_5<VAR>Ring C<VAR>TopologicalSpace C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>f : B →A[S] C<GOAL>⇑(ContinuousAlgHom.restrictScalars R f) = ⇑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>s : Subalgebra R A<GOAL>s ≤ s.topologicalClosure
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>s : Subalgebra R A<GOAL>IsClosed ↑s.topologicalClosure
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>s : Subalgebra R A<VAR>t : Subalgebra R A<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>s : Subalgebra R A<VAR>B : Type u_2<VAR>TopologicalSpace B<VAR>Ring B<VAR>TopologicalRing B<VAR>Algebra R B<VAR>f : B →ₐ[R] A<VAR>f' : B ≃ₜ A<VAR>w : ⇑f = ⇑f'<GOAL>Subalgebra.comap f s.topologicalClosure = (Subalgebra.comap f s).topologicalClosure
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u<VAR>TopologicalSpace A<VAR>Ring A<VAR>Algebra R A<VAR>TopologicalRing A<VAR>x : A<GOAL>x ∈ Algebra.elementalAlgebra R x
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>𝔖 : Set (Set E)<GOAL>UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 = TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>𝔖 : Set (Set E)<GOAL>UniformConvergenceCLM.instUniformSpace σ F 𝔖 = UniformSpace.comap DFunLike.coe (UniformOnFun.uniformSpace E F 𝔖)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>𝔖 : Set (Set E)<GOAL>UniformSpace.toTopologicalSpace = UniformConvergenceCLM.instTopologicalSpace σ F 𝔖
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>𝔖 : Set (Set E)<GOAL>UniformEmbedding DFunLike.coe
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>𝔖 : Set (Set E)<GOAL>Embedding (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>T2Space F<VAR>𝔖 : Set (Set E)<VAR>h𝔖 : ⋃₀ 𝔖 = Set.univ<GOAL>T2Space (UniformConvergenceCLM σ F 𝔖)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>RingHomSurjective σ<VAR>RingHomIsometric σ<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜₂ F<VAR>𝔖 : Set (Set E)<VAR>h𝔖₃ : ∀ S ∈ 𝔖, Bornology.IsVonNBounded 𝕜₁ S<GOAL>ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ι : Type u_5<VAR>𝔖 : Set (Set E)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<GOAL>(𝓝 0).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>𝔖 : Set (Set E)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<GOAL>(𝓝 0).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓝 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>ι : Type u_5<VAR>p : Filter ι<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>𝔖 : Set (Set E)<VAR>a : ι → UniformConvergenceCLM σ F 𝔖<VAR>a₀ : UniformConvergenceCLM σ F 𝔖<GOAL>Filter.Tendsto a p (𝓝 a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x x_1 => (a x) x_1) (⇑a₀) p s
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>𝔖₁ 𝔖₂ : Set (Set E)<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>h : 𝔖₂ ⊆ 𝔖₁<GOAL>UniformConvergenceCLM.instUniformSpace σ F 𝔖₁ ≤ UniformConvergenceCLM.instUniformSpace σ F 𝔖₂
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>𝔖₁ 𝔖₂ : Set (Set E)<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>h : 𝔖₂ ⊆ 𝔖₁<GOAL>UniformConvergenceCLM.instTopologicalSpace σ F 𝔖₁ ≤ UniformConvergenceCLM.instTopologicalSpace σ F 𝔖₂
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ι : Type u_7<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<GOAL>(𝓝 0).HasBasis (fun Si => Bornology.IsVonNBounded 𝕜₁ Si.1 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<GOAL>(𝓝 0).HasBasis (fun SV => Bornology.IsVonNBounded 𝕜₁ SV.1 ∧ SV.2 ∈ 𝓝 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>AddCommGroup G<VAR>Module 𝕜₃ G<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ContinuousConstSMul 𝕜₃ G<VAR>RingHomSurjective σ<VAR>RingHomIsometric σ<VAR>L : E →SL[σ] F<VAR>f : F →SL[τ] G<GOAL>(ContinuousLinearMap.precomp G L) f = f.comp L
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>AddCommGroup G<VAR>Module 𝕜₃ G<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalSpace G<VAR>TopologicalAddGroup F<VAR>TopologicalAddGroup G<VAR>ContinuousConstSMul 𝕜₃ G<VAR>ContinuousConstSMul 𝕜₂ F<VAR>L : F →SL[τ] G<VAR>f : E →SL[σ] F<GOAL>(ContinuousLinearMap.postcomp E L) f = L.comp f
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>AddCommGroup G<VAR>Module 𝕜 G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ContinuousConstSMul 𝕜 G<VAR>L : E →L[𝕜] F →L[𝕜] G<VAR>v : E<VAR>w : F<GOAL>(L.toLinearMap₂ v) w = (L v) w
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>𝕜₄ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NontriviallyNormedField 𝕜₄<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>Module 𝕜₃ G<VAR>Module 𝕜₄ H<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalSpace G<VAR>TopologicalSpace H<VAR>TopologicalAddGroup G<VAR>TopologicalAddGroup H<VAR>ContinuousConstSMul 𝕜₃ G<VAR>ContinuousConstSMul 𝕜₄ H<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>σ₃₄ : 𝕜₃ →+* 𝕜₄<VAR>σ₄₃ : 𝕜₄ →+* 𝕜₃<VAR>σ₂₄ : 𝕜₂ →+* 𝕜₄<VAR>σ₁₄ : 𝕜 →+* 𝕜₄<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₃₄ σ₄₃<VAR>RingHomInvPair σ₄₃ σ₃₄<VAR>RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>RingHomIsometric σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>e₁₂ : E ≃SL[σ₁₂] F<VAR>e₄₃ : H ≃SL[σ₄₃] G<VAR>L : F →SL[σ₂₃] G<GOAL>(e₁₂.arrowCongrSL e₄₃).symm L = (↑e₄₃.symm).comp (L.comp ↑e₁₂)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>𝕜₄ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NontriviallyNormedField 𝕜₄<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>Module 𝕜₃ G<VAR>Module 𝕜₄ H<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalSpace G<VAR>TopologicalSpace H<VAR>TopologicalAddGroup G<VAR>TopologicalAddGroup H<VAR>ContinuousConstSMul 𝕜₃ G<VAR>ContinuousConstSMul 𝕜₄ H<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>σ₃₄ : 𝕜₃ →+* 𝕜₄<VAR>σ₄₃ : 𝕜₄ →+* 𝕜₃<VAR>σ₂₄ : 𝕜₂ →+* 𝕜₄<VAR>σ₁₄ : 𝕜 →+* 𝕜₄<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₃₄ σ₄₃<VAR>RingHomInvPair σ₄₃ σ₃₄<VAR>RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>RingHomIsometric σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>e₁₂ : E ≃SL[σ₁₂] F<VAR>e₄₃ : H ≃SL[σ₄₃] G<VAR>L : E →SL[σ₁₄] H<GOAL>(e₁₂.arrowCongrSL e₄₃) L = (↑e₄₃).comp (L.comp ↑e₁₂.symm)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>𝕜₄ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NontriviallyNormedField 𝕜₄<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>Module 𝕜₃ G<VAR>Module 𝕜₄ H<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalSpace G<VAR>TopologicalSpace H<VAR>TopologicalAddGroup G<VAR>TopologicalAddGroup H<VAR>ContinuousConstSMul 𝕜₃ G<VAR>ContinuousConstSMul 𝕜₄ H<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>σ₃₄ : 𝕜₃ →+* 𝕜₄<VAR>σ₄₃ : 𝕜₄ →+* 𝕜₃<VAR>σ₂₄ : 𝕜₂ →+* 𝕜₄<VAR>σ₁₄ : 𝕜 →+* 𝕜₄<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomInvPair σ₃₄ σ₄₃<VAR>RingHomInvPair σ₄₃ σ₃₄<VAR>RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>RingHomIsometric σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>e₁₂ : E ≃SL[σ₁₂] F<VAR>e₄₃ : H ≃SL[σ₄₃] G<VAR>L : E →SL[σ₁₄] H<GOAL>(e₁₂.arrowCongrSL e₄₃).toLinearEquiv L = (↑e₄₃).comp (L.comp ↑e₁₂.symm)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>NontriviallyNormedField 𝕜<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module 𝕜 G<VAR>Module 𝕜 H<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalSpace G<VAR>TopologicalSpace H<VAR>TopologicalAddGroup G<VAR>TopologicalAddGroup H<VAR>ContinuousConstSMul 𝕜 G<VAR>ContinuousConstSMul 𝕜 H<VAR>e₁ : E ≃L[𝕜] F<VAR>e₂ : H ≃L[𝕜] G<VAR>f : E →L[𝕜] H<VAR>x : F<GOAL>((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>NontriviallyNormedField 𝕜<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module 𝕜 G<VAR>Module 𝕜 H<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>TopologicalSpace G<VAR>TopologicalSpace H<VAR>TopologicalAddGroup G<VAR>TopologicalAddGroup H<VAR>ContinuousConstSMul 𝕜 G<VAR>ContinuousConstSMul 𝕜 H<VAR>e₁ : E ≃L[𝕜] F<VAR>e₂ : H ≃L[𝕜] G<GOAL>(e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
<VAR>α : Type u_1<GOAL>Specialization.toEquiv.symm = Specialization.ofEquiv
<VAR>α : Type u_1<GOAL>Specialization.ofEquiv.symm = Specialization.toEquiv
<VAR>α : Type u_1<VAR>a : Specialization α<GOAL>Specialization.toEquiv (Specialization.ofEquiv a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>Specialization.ofEquiv (Specialization.toEquiv a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>Specialization.toEquiv a = Specialization.toEquiv b ↔ a = b
<VAR>α : Type u_1<VAR>a b : Specialization α<GOAL>Specialization.ofEquiv a = Specialization.ofEquiv b ↔ a = b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a b : α<GOAL>Specialization.toEquiv a ≤ Specialization.toEquiv b ↔ b ⤳ a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a b : Specialization α<GOAL>Specialization.ofEquiv a ⤳ Specialization.ofEquiv b ↔ b ≤ a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>s : Set (Specialization α)<GOAL>IsOpen (⇑Specialization.toEquiv ⁻¹' s) ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>s : Set α<GOAL>IsUpperSet (⇑Specialization.ofEquiv ⁻¹' s) ↔ IsOpen s
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>Specialization.map (ContinuousMap.id α) = OrderHom.id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : C(β, γ)<VAR>f : C(α, β)<GOAL>Specialization.map (g.comp f) = (Specialization.map g).comp (Specialization.map f)
<GOAL>∀ {X Y : TopCat} (f : C(↑X, ↑Y)), topToPreord.map f = Specialization.map f
<VAR>X : TopCat<GOAL>topToPreord.obj X = Preord.of (Specialization ↑X)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>self : ProperVAdd G X<GOAL>IsProperMap fun gx => (gx.1 +ᵥ gx.2, gx.2)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>Group G<VAR>MulAction G X<VAR>self : ProperSMul G X<GOAL>IsProperMap fun gx => (gx.1 • gx.2, gx.2)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>AddGroup G<VAR>AddAction G X<GOAL>ProperVAdd G X ↔ IsProperMap fun gx => (gx.1 +ᵥ gx.2, gx.2)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>Group G<VAR>MulAction G X<GOAL>ProperSMul G X ↔ IsProperMap fun gx => (gx.1 • gx.2, gx.2)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>AddGroup G<VAR>AddAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<GOAL>ProperVAdd G X ↔ ContinuousVAdd G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun gx => (gx.1 +ᵥ gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g +ᵥ x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (𝓝 g)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<GOAL>ProperSMul G X ↔ ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (𝓝 g)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>T2Space X<GOAL>ProperSMul G X ↔ ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Filter.Tendsto Prod.fst (↑𝒰) (𝓝 g)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>AddGroup G<VAR>AddAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>ProperVAdd G X<GOAL>T2Space (Quotient (AddAction.orbitRel G X))
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>ProperSMul G X<GOAL>T2Space (Quotient (MulAction.orbitRel G X))
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>TopologicalSpace G<VAR>TopologicalSpace X<VAR>h_proper : ProperSMul G X<VAR>T2Space G<GOAL>T2Space X