ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>⇑1 = id
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>f g : P →ᵃⁱ[𝕜] P<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace 𝕜 P<VAR>Nonempty ↥s<GOAL>s.subtypeₐᵢ.linear = s.direction.subtype
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace 𝕜 P<VAR>Nonempty ↥s<GOAL>s.subtypeₐᵢ.linearIsometry = s.direction.subtypeₗᵢ
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace 𝕜 P<VAR>Nonempty ↥s<GOAL>⇑s.subtypeₐᵢ = ⇑s.subtype
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace 𝕜 P<VAR>Nonempty ↥s<GOAL>s.subtypeₐᵢ.toAffineMap = s.subtype
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>self : P ≃ᵃⁱ[𝕜] P₂<VAR>x : V<GOAL>‖self.linear x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>e.linear = e.linearIsometryEquiv.toLinearEquiv
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃ[𝕜] P₂<VAR>he : ∀ (x : V), ‖e.linear x‖ = ‖x‖<GOAL>⇑{ toAffineEquiv := e, norm_map := he } = ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>⇑e.toAffineEquiv = ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<GOAL>Function.Injective AffineIsometryEquiv.toAffineEquiv
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e e' : P ≃ᵃⁱ[𝕜] P₂<VAR>h : ∀ (x : P), e x = e' x<GOAL>e = e'
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>⇑e.toAffineIsometry = ⇑e
<VAR>𝕜 : Type u_1<VAR>V₁ : Type u_3<VAR>V₂ : Type u_5<VAR>P₁ : Type u_8<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V₁<VAR>NormedSpace 𝕜 V₁<VAR>PseudoMetricSpace P₁<VAR>NormedAddTorsor V₁ P₁<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P₁ → P₂<VAR>e' : V₁ ≃ₗᵢ[𝕜] V₂<VAR>p : P₁<VAR>h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p<GOAL>⇑(AffineIsometryEquiv.mk' e e' p h) = e
<VAR>𝕜 : Type u_1<VAR>V₁ : Type u_3<VAR>V₂ : Type u_5<VAR>P₁ : Type u_8<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V₁<VAR>NormedSpace 𝕜 V₁<VAR>PseudoMetricSpace P₁<VAR>NormedAddTorsor V₁ P₁<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P₁ → P₂<VAR>e' : V₁ ≃ₗᵢ[𝕜] V₂<VAR>p : P₁<VAR>h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p<GOAL>(AffineIsometryEquiv.mk' e e' p h).linearIsometryEquiv = e'
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>e : V ≃ₗᵢ[𝕜] V₂<GOAL>⇑e.toAffineIsometryEquiv = ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>e : V ≃ₗᵢ[𝕜] V₂<GOAL>e.toAffineIsometryEquiv.linearIsometryEquiv = e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>e : V ≃ₗᵢ[𝕜] V₂<GOAL>e.toAffineIsometryEquiv.toAffineEquiv = e.toAffineEquiv
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>e : V ≃ₗᵢ[𝕜] V₂<GOAL>e.toAffineIsometryEquiv.toAffineIsometry = e.toLinearIsometry.toAffineIsometry
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>Isometry ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>⇑e.toIsometryEquiv = ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>Set.range ⇑e = Set.univ
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>⇑e.toHomeomorph = ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>Continuous ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>x : P<GOAL>ContinuousAt (⇑e) x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>s : Set P<GOAL>ContinuousOn (⇑e) s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>s : Set P<VAR>x : P<GOAL>ContinuousWithinAt (⇑e) s x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>⇑(AffineIsometryEquiv.refl 𝕜 P) = id
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>(AffineIsometryEquiv.refl 𝕜 P).toAffineEquiv = AffineEquiv.refl 𝕜 P
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>(AffineIsometryEquiv.refl 𝕜 P).toIsometryEquiv = IsometryEquiv.refl P
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>(AffineIsometryEquiv.refl 𝕜 P).toHomeomorph = Homeomorph.refl P
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>x : P₂<GOAL>e (e.symm x) = x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>x : P<GOAL>e.symm (e x) = x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>e.symm.symm = e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>e.symm = e.symm.toAffineEquiv
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>e.toIsometryEquiv.symm = e.symm.toIsometryEquiv
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>e.toHomeomorph.symm = e.symm.toHomeomorph
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>SeminormedAddCommGroup V₃<VAR>NormedSpace 𝕜 V₃<VAR>PseudoMetricSpace P₃<VAR>NormedAddTorsor V₃ P₃<VAR>e₁ : P ≃ᵃⁱ[𝕜] P₂<VAR>e₂ : P₂ ≃ᵃⁱ[𝕜] P₃<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>e.trans (AffineIsometryEquiv.refl 𝕜 P₂) = e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>(AffineIsometryEquiv.refl 𝕜 P).trans e = e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>e.trans e.symm = AffineIsometryEquiv.refl 𝕜 P
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>e.symm.trans e = AffineIsometryEquiv.refl 𝕜 P₂
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>SeminormedAddCommGroup V₃<VAR>NormedSpace 𝕜 V₃<VAR>PseudoMetricSpace P₃<VAR>NormedAddTorsor V₃ P₃<VAR>e₁ : P ≃ᵃⁱ[𝕜] P₂<VAR>e₂ : P₂ ≃ᵃⁱ[𝕜] P₃<GOAL>⇑(e₁.trans e₂).symm = ⇑e₁.symm ∘ ⇑e₂.symm
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>SeminormedAddCommGroup V₃<VAR>NormedSpace 𝕜 V₃<VAR>PseudoMetricSpace P₃<VAR>NormedAddTorsor V₃ P₃<VAR>SeminormedAddCommGroup V₄<VAR>NormedSpace 𝕜 V₄<VAR>PseudoMetricSpace P₄<VAR>NormedAddTorsor V₄ P₄<VAR>ePP₂ : P ≃ᵃⁱ[𝕜] P₂<VAR>eP₂G : P₂ ≃ᵃⁱ[𝕜] P₃<VAR>eGG' : P₃ ≃ᵃⁱ[𝕜] P₄<GOAL>ePP₂.trans (eP₂G.trans eGG') = (ePP₂.trans eP₂G).trans eGG'
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>e e' : P ≃ᵃⁱ[𝕜] P<GOAL>⇑(e * e') = ⇑e ∘ ⇑e'
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>e : P ≃ᵃⁱ[𝕜] P<GOAL>⇑e⁻¹ = ⇑e.symm
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>p : P<VAR>v : V<GOAL>e (v +ᵥ p) = e.linearIsometryEquiv v +ᵥ e p
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>p1 p2 : P<GOAL>e.linearIsometryEquiv (p1 -ᵥ p2) = e p1 -ᵥ e p2
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>dist (e x) (e y) = dist x y
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>edist (e x) (e y) = edist x y
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>Function.Bijective ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>Function.Injective ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>Function.Surjective ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>e x = e y ↔ x = y
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>x y : P<VAR>h : x ≠ y<GOAL>e x ≠ e y
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>LipschitzWith 1 ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<GOAL>AntilipschitzWith 1 ⇑e
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>s : Set P<GOAL>EMetric.diam (⇑e '' s) = EMetric.diam s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>s : Set P<GOAL>Metric.diam (⇑e '' s) = Metric.diam s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>α : Type u_14<VAR>TopologicalSpace α<VAR>f : α → P<VAR>s : Set α<GOAL>ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>α : Type u_14<VAR>TopologicalSpace α<VAR>f : α → P<GOAL>Continuous (⇑e ∘ f) ↔ Continuous f
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<GOAL>⇑(AffineIsometryEquiv.vaddConst 𝕜 p) = fun v => v +ᵥ p
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<GOAL>⇑(AffineEquiv.vaddConst 𝕜 p) = fun v => v +ᵥ p
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<GOAL>⇑(AffineIsometryEquiv.vaddConst 𝕜 p).symm = fun p' => p' -ᵥ p
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<GOAL>(AffineIsometryEquiv.vaddConst 𝕜 p).toAffineEquiv = AffineEquiv.vaddConst 𝕜 p
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<GOAL>⇑(AffineIsometryEquiv.constVSub 𝕜 p) = fun x => p -ᵥ x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<GOAL>(AffineIsometryEquiv.constVSub 𝕜 p).symm = (LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (AffineIsometryEquiv.vaddConst 𝕜 p)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v : V<GOAL>⇑(AffineIsometryEquiv.constVAdd 𝕜 P v) = fun x => v +ᵥ x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>AffineIsometryEquiv.constVAdd 𝕜 P 0 = AffineIsometryEquiv.refl 𝕜 P
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₂ : Type u_5<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>f : P → P₂<VAR>hf : Isometry f<VAR>p : P<VAR>g : V → V₂<VAR>hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p<GOAL>Isometry g
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x y : P<GOAL>(AffineIsometryEquiv.pointReflection 𝕜 x) y = x -ᵥ y +ᵥ x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_10<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x : P<GOAL>(AffineIsometryEquiv.pointReflection 𝕜 x).toAffineEquiv = AffineEquiv.pointReflection 𝕜 x