ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<GOAL>Function.Bijective ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<GOAL>Function.Injective ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<GOAL>Function.Surjective ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>e₁ : M₁ ≃SL[σ₁₂] M₂<VAR>e₂ : M₂ ≃SL[σ₂₃] M₃<VAR>c : M₁<GOAL>(e₁.trans e₂) c = e₂ (e₁ c)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>c : M₂<GOAL>e (e.symm c) = c
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>b : M₁<GOAL>e.symm (e b) = b
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>e₁ : M₂ ≃SL[σ₂₁] M₁<VAR>e₂ : M₃ ≃SL[σ₃₂] M₂<VAR>c : M₁<GOAL>(e₂.trans e₁).symm c = e₂.symm (e₁.symm c)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₁<GOAL>⇑e.symm '' (⇑e '' s) = s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₂<GOAL>⇑e '' (⇑e.symm '' s) = s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>f : M₁ ≃SL[σ₁₂] M₂<VAR>f' : M₂ ≃SL[σ₂₃] M₃<GOAL>(↑f').comp ↑f = ↑(f.trans f')
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<GOAL>(↑e).comp ↑e.symm = ContinuousLinearMap.id R₂ M₂
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<GOAL>(↑e.symm).comp ↑e = ContinuousLinearMap.id R₁ M₁
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<GOAL>⇑e.symm ∘ ⇑e = id
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<GOAL>⇑e ∘ ⇑e.symm = id
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<GOAL>e.symm.symm = e
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<GOAL>(ContinuousLinearEquiv.refl R₁ M₁).symm = ContinuousLinearEquiv.refl R₁ M₁
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₁<GOAL>e.symm.symm x = e x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₂<VAR>y : M₁<GOAL>e.symm x = y ↔ x = e y
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₂<VAR>y : M₁<GOAL>y = e.symm x ↔ e y = x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₁<GOAL>⇑e '' s = ⇑e.symm ⁻¹' s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₂<GOAL>⇑e.symm '' s = ⇑e ⁻¹' s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₂<GOAL>⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>s : Set M₁<GOAL>⇑e ⁻¹' (⇑e.symm ⁻¹' s) = s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>E₁ : Type u_9<VAR>E₂ : Type u_10<VAR>UniformSpace E₁<VAR>UniformSpace E₂<VAR>AddCommGroup E₁<VAR>AddCommGroup E₂<VAR>Module R₁ E₁<VAR>Module R₂ E₂<VAR>UniformAddGroup E₁<VAR>UniformAddGroup E₂<VAR>e : E₁ ≃SL[σ₁₂] E₂<GOAL>UniformEmbedding ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>E₁ : Type u_9<VAR>E₂ : Type u_10<VAR>UniformSpace E₁<VAR>UniformSpace E₂<VAR>AddCommGroup E₁<VAR>AddCommGroup E₂<VAR>Module R₁ E₁<VAR>Module R₂ E₂<VAR>UniformAddGroup E₁<VAR>UniformAddGroup E₂<VAR>e : E₁ ≃ₛₗ[σ₁₂] E₂<VAR>h₁ : Continuous ⇑e<VAR>h₂ : Continuous ⇑e.symm<GOAL>UniformEmbedding ⇑e
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f₁ : M₁ →SL[σ₁₂] M₂<VAR>f₂ : M₂ →SL[σ₂₁] M₁<VAR>h₁ : Function.LeftInverse ⇑f₂ ⇑f₁<VAR>h₂ : Function.RightInverse ⇑f₂ ⇑f₁<VAR>x : M₁<GOAL>(ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂) x = f₁ x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f₁ : M₁ →SL[σ₁₂] M₂<VAR>f₂ : M₂ →SL[σ₂₁] M₁<VAR>h₁ : Function.LeftInverse ⇑f₂ ⇑f₁<VAR>h₂ : Function.RightInverse ⇑f₂ ⇑f₁<GOAL>(ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂).symm = ContinuousLinearEquiv.equivOfInverse f₂ f₁ h₂ h₁
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>TopologicalSpace M₄<VAR>AddCommMonoid M₄<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>R₄ : Type u_9<VAR>Semiring R₄<VAR>Module R₄ M₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>σ₄₃ : R₄ →+* R₃<VAR>RingHomInvPair σ₃₄ σ₄₃<VAR>RingHomInvPair σ₄₃ σ₃₄<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₁₄ : R₁ →+* R₄<VAR>RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>e₁₂ : M₁ ≃SL[σ₁₂] M₂<VAR>e₄₃ : M₄ ≃SL[σ₄₃] M₃<VAR>f : M₂ →SL[σ₂₃] M₃<GOAL>(e₁₂.arrowCongrEquiv e₄₃).symm f = (↑e₄₃.symm).comp (f.comp ↑e₁₂)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>TopologicalSpace M₄<VAR>AddCommMonoid M₄<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>R₄ : Type u_9<VAR>Semiring R₄<VAR>Module R₄ M₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>σ₄₃ : R₄ →+* R₃<VAR>RingHomInvPair σ₃₄ σ₄₃<VAR>RingHomInvPair σ₄₃ σ₃₄<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₁₄ : R₁ →+* R₄<VAR>RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>e₁₂ : M₁ ≃SL[σ₁₂] M₂<VAR>e₄₃ : M₄ ≃SL[σ₄₃] M₃<VAR>f : M₁ →SL[σ₁₄] M₄<GOAL>(e₁₂.arrowCongrEquiv e₄₃) f = (↑e₄₃).comp (f.comp ↑e₁₂.symm)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_3<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_4<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>M₄ : Type u_5<VAR>TopologicalSpace M₄<VAR>AddCommGroup M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>TopologicalAddGroup M₄<VAR>e : M ≃L[R] M₂<VAR>e' : M₃ ≃L[R] M₄<VAR>f : M →L[R] M₄<VAR>x : M × M₃<GOAL>(e.skewProd e' f) x = (e x.1, e' x.2 + f x.1)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_3<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>M₃ : Type u_4<VAR>TopologicalSpace M₃<VAR>AddCommGroup M₃<VAR>M₄ : Type u_5<VAR>TopologicalSpace M₄<VAR>AddCommGroup M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>TopologicalAddGroup M₄<VAR>e : M ≃L[R] M₂<VAR>e' : M₃ ≃L[R] M₄<VAR>f : M →L[R] M₄<VAR>x : M₂ × M₄<GOAL>(e.skewProd e' f).symm x = (e.symm x.1, e'.symm (x.2 - f (e.symm x.1)))
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>e : M ≃SL[σ₁₂] M₂<VAR>x y : M<GOAL>e (x - y) = e x - e y
<VAR>R : Type u_1<VAR>Ring R<VAR>R₂ : Type u_2<VAR>Ring R₂<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>e : M ≃SL[σ₁₂] M₂<VAR>x : M<GOAL>e (-x) = -e x
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>f : (M →L[R] M)ˣ<VAR>x : M<GOAL>((ContinuousLinearEquiv.unitsEquiv R M) f) x = ↑f x
<VAR>R : Type u_1<VAR>Ring R<VAR>TopologicalSpace R<VAR>ContinuousMul R<VAR>u : Rˣ<VAR>x : R<GOAL>((ContinuousLinearEquiv.unitsEquivAut R) u) x = x * ↑u
<VAR>R : Type u_1<VAR>Ring R<VAR>TopologicalSpace R<VAR>ContinuousMul R<VAR>u : Rˣ<VAR>x : R<GOAL>((ContinuousLinearEquiv.unitsEquivAut R) u).symm x = x * ↑u⁻¹
<VAR>R : Type u_1<VAR>Ring R<VAR>TopologicalSpace R<VAR>ContinuousMul R<VAR>e : R ≃L[R] R<GOAL>↑((ContinuousLinearEquiv.unitsEquivAut R).symm e) = e 1
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>TopologicalAddGroup M<VAR>f₁ : M →L[R] M₂<VAR>f₂ : M₂ →L[R] M<VAR>h : Function.RightInverse ⇑f₂ ⇑f₁<VAR>x : M<GOAL>((ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h) x).1 = f₁ x
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>TopologicalAddGroup M<VAR>f₁ : M →L[R] M₂<VAR>f₂ : M₂ →L[R] M<VAR>h : Function.RightInverse ⇑f₂ ⇑f₁<VAR>x : M<GOAL>↑((ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h) x).2 = x - f₂ (f₁ x)
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>TopologicalAddGroup M<VAR>f₁ : M →L[R] M₂<VAR>f₂ : M₂ →L[R] M<VAR>h : Function.RightInverse ⇑f₂ ⇑f₁<VAR>y : M₂ × ↥(LinearMap.ker f₁)<GOAL>(ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h).symm y = f₂ y.1 + ↑y.2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Unique ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<GOAL>⇑(ContinuousLinearEquiv.funUnique ι R M) = Function.eval default
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Unique ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<GOAL>⇑(ContinuousLinearEquiv.funUnique ι R M).symm = Function.const ι
<VAR>R : Type u_2<VAR>Semiring R<VAR>M : Fin 2 → Type u_4<VAR>(i : Fin 2) → AddCommMonoid (M i)<VAR>(i : Fin 2) → Module R (M i)<VAR>(i : Fin 2) → TopologicalSpace (M i)<GOAL>⇑(ContinuousLinearEquiv.piFinTwo R M).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
<VAR>R : Type u_2<VAR>Semiring R<VAR>M : Fin 2 → Type u_4<VAR>(i : Fin 2) → AddCommMonoid (M i)<VAR>(i : Fin 2) → Module R (M i)<VAR>(i : Fin 2) → TopologicalSpace (M i)<GOAL>⇑(ContinuousLinearEquiv.piFinTwo R M) = fun f => (f 0, f 1)
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<GOAL>⇑(ContinuousLinearEquiv.finTwoArrow R M) = fun f => (f 0, f 1)
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<GOAL>⇑(ContinuousLinearEquiv.finTwoArrow R M).symm = fun x => ![x.1, x.2]
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : M ≃L[R] M₂<GOAL>(↑e).inverse = ↑e.symm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M →L[R] M₂<VAR>h : ¬∃ e', ↑e' = f<GOAL>f.inverse = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : M ≃L[R] M<GOAL>Ring.inverse ↑e = (↑e).inverse
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace M₂<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>e : M ≃L[R] M₂<VAR>f : M →L[R] M₂<GOAL>f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Ring.inverse = ContinuousLinearMap.inverse
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>T1Space ↥p<VAR>h : p.ClosedComplemented<GOAL>∃ q, IsClosed ↑q ∧ IsCompl p q
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalAddGroup M<VAR>T1Space M<VAR>p : Submodule R M<VAR>h : p.ClosedComplemented<GOAL>IsClosed ↑p
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<GOAL>⊥.ClosedComplemented
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<GOAL>⊤.ClosedComplemented
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalAddGroup M<VAR>p : Submodule R M<VAR>hp : p.ClosedComplemented<GOAL>∃ q e, (∀ (x : ↥p), e ↑x = (x, 0)) ∧ (∀ (y : ↥q), e ↑y = (0, y)) ∧ ∀ (x : ↥p × ↥q), e.symm x = ↑x.1 + ↑x.2
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>M₂ : Type u_3<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>TopologicalAddGroup M<VAR>f₁ : M →L[R] M₂<VAR>f₂ : M₂ →L[R] M<VAR>h : Function.RightInverse ⇑f₂ ⇑f₁<GOAL>(LinearMap.ker f₁).ClosedComplemented
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace M<VAR>S : Submodule R M<VAR>TopologicalAddGroup M<GOAL>IsOpenMap ⇑S.mkQ
<GOAL>Equivalence GromovHausdorff.IsometryRel
<VAR>X : Type u<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>p : TopologicalSpace.NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)<GOAL>⟦p⟧ = GromovHausdorff.toGHSpace X ↔ ∃ Ψ, Isometry Ψ ∧ Set.range Ψ = ↑p
<VAR>p : TopologicalSpace.NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)<GOAL>⟦p⟧ = GromovHausdorff.toGHSpace ↥p
<VAR>p : GromovHausdorff.GHSpace<GOAL>GromovHausdorff.toGHSpace p.Rep = p
<VAR>X : Type u<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>Y : Type v<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>GromovHausdorff.toGHSpace X = GromovHausdorff.toGHSpace Y ↔ Nonempty (X ≃ᵢ Y)
<VAR>p q : GromovHausdorff.GHSpace<GOAL>dist p q = GromovHausdorff.ghDist p.Rep q.Rep
<VAR>X : Type u<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>Y : Type v<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<VAR>γ : Type w<VAR>MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<GOAL>GromovHausdorff.ghDist X Y ≤ Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)
<VAR>X : Type u<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>Y : Type v<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y)) (Set.range (GromovHausdorff.optimalGHInjr X Y)) = GromovHausdorff.ghDist X Y
<VAR>X : Type u<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>Y : Type v<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ GromovHausdorff.ghDist X Y = Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)
<VAR>X : Type u<VAR>MetricSpace X<VAR>p q : TopologicalSpace.NonemptyCompacts X<GOAL>dist p.toGHSpace q.toGHSpace ≤ dist p q
<VAR>X : Type u<VAR>MetricSpace X<GOAL>LipschitzWith 1 TopologicalSpace.NonemptyCompacts.toGHSpace
<VAR>X : Type u<VAR>MetricSpace X<GOAL>Continuous TopologicalSpace.NonemptyCompacts.toGHSpace
<VAR>X : Type u<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>Y : Type v<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<GOAL>GromovHausdorff.ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃
<VAR>t : Set GromovHausdorff.GHSpace<VAR>C : ℝ<VAR>u : ℕ → ℝ<VAR>K : ℕ → ℕ<VAR>ulim : Filter.Tendsto u Filter.atTop (𝓝 0)<VAR>hdiam : ∀ p ∈ t, Metric.diam Set.univ ≤ C<VAR>hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ Set.univ ⊆ ⋃ x ∈ s, Metric.ball x (u n)<GOAL>TotallyBounded t
<VAR>A : Type<VAR>MetricSpace A<VAR>self : GromovHausdorff.AuxGluingStruct A<GOAL>Isometry self.embed
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<GOAL>EuclideanGeometry.inversion = fun c R x => (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c : P<VAR>R : ℝ<VAR>x : P<GOAL>EuclideanGeometry.inversion c R x = (AffineMap.lineMap c x) ((R / dist x c) ^ 2)