ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<GOAL>∀ᶠ (p : F × ↥(LinearMap.ker f')) in 𝓝 (f a, 0), f (HasStrictFDerivAt.implicitFunction f f' hf hf' p.1 p.2) = p.1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<GOAL>HasStrictFDerivAt.implicitFunction f f' hf hf' (f a) 0 = a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<GOAL>∀ᶠ (x : E) in 𝓝 a, HasStrictFDerivAt.implicitFunction f f' hf hf' (f x) (↑(HasStrictFDerivAt.implicitToPartialHomeomorph f f' hf hf') x).2 = x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<GOAL>HasStrictFDerivAt (HasStrictFDerivAt.implicitFunction f f' hf hf' (f a)) (LinearMap.ker f').subtypeL 0
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>μ : MeasureTheory.Measure ℝ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lip : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (Metric.ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt (fun x => F x t) (F' t) x₀<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>μ : MeasureTheory.Measure ℝ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ Metric.ball x₀ ε, ‖F' x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ Metric.ball x₀ ε, HasFDerivAt (fun x => F x t) (F' x t) x<GOAL>HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>μ : MeasureTheory.Measure ℝ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : 𝕜 → ℝ → E<VAR>F' : ℝ → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lipsch : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (Metric.ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasDerivAt (fun x => F x t) (F' t) x₀<GOAL>IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>μ : MeasureTheory.Measure ℝ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F F' : 𝕜 → ℝ → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ Metric.ball x₀ ε, ‖F' x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ Metric.ball x₀ ε, HasDerivAt (fun x => F x t) (F' x t) x<GOAL>IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>E : Type u_11<VAR>E₂ : Type u_12<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>self : E →ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>‖self.toLinearMap x‖ = ‖x‖
<VAR>𝓕 : Type u_11<VAR>R : outParam (Type u_12)<VAR>R₂ : outParam (Type u_13)<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : outParam (R →+* R₂)<VAR>E : outParam (Type u_14)<VAR>E₂ : outParam (Type u_15)<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>self : SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<VAR>x : E<GOAL>‖f x‖ = ‖x‖
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<GOAL>Isometry ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<GOAL>Continuous ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<VAR>x : E<GOAL>‖f x‖₊ = ‖x‖₊
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<GOAL>LipschitzWith 1 ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<GOAL>AntilipschitzWith 1 ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<VAR>s : Set E<GOAL>EMetric.diam (⇑f '' s) = EMetric.diam s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<GOAL>EMetric.diam (Set.range ⇑f) = EMetric.diam Set.univ
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<VAR>s : Set E<GOAL>Metric.diam (⇑f '' s) = Metric.diam s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<GOAL>Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective LinearIsometry.toLinearMap
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E →ₛₗᵢ[σ₁₂] E₂<GOAL>f.toLinearMap = g.toLinearMap ↔ f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>⇑f.toLinearMap = ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>hf : ∀ (x : E), ‖f x‖ = ‖x‖<GOAL>⇑{ toLinearMap := f, norm_map' := hf } = ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective fun f => ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E →ₛₗᵢ[σ₁₂] E₂<VAR>h : ∀ (x : E), f x = g x<GOAL>f = g
<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>FunLike 𝓕 E E₂<VAR>f : 𝓕<VAR>x x' : E<GOAL>x = x' → f x = f x'
<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>FunLike 𝓕 E E₂<VAR>f g : 𝓕<VAR>h : f = g<VAR>x : E<GOAL>f x = g x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>f 0 = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>f (x + y) = f x + f y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>f (-x) = -f x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>f (x - y) = f x - f y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>c : R<VAR>x : E<GOAL>f (c • x) = σ₁₂ c • f x
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R E₂<VAR>f : E →ₗᵢ[R] E₂<VAR>c : R<VAR>x : E<GOAL>f (c • x) = c • f x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>‖f x‖ = ‖x‖
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>‖f x‖₊ = ‖x‖₊
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>Isometry ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<VAR>s : Set E<GOAL>IsComplete (⇑f '' s) ↔ IsComplete s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>s : Set E<GOAL>IsComplete (⇑f '' s) ↔ IsComplete s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>RingHomSurjective σ₁₂<VAR>p : Submodule R E<GOAL>IsComplete ↑(Submodule.map f.toLinearMap p) ↔ IsComplete ↑p
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>𝓕 : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>FunLike 𝓕 E E₂<VAR>SemilinearIsometryClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<VAR>RingHomSurjective σ₁₂<VAR>p : Submodule R E<GOAL>IsComplete ↑(Submodule.map f p) ↔ IsComplete ↑p
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>dist (f x) (f y) = dist x y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>edist (f x) (f y) = edist x y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E₂ : Type u_6<VAR>F : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E₂<VAR>Module R₂ E₂<VAR>NormedAddCommGroup F<VAR>Module R F<VAR>f₁ : F →ₛₗᵢ[σ₁₂] E₂<GOAL>Function.Injective ⇑f₁
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E₂ : Type u_6<VAR>F : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E₂<VAR>Module R₂ E₂<VAR>NormedAddCommGroup F<VAR>Module R F<VAR>f₁ : F →ₛₗᵢ[σ₁₂] E₂<VAR>x y : F<GOAL>f₁ x = f₁ y ↔ x = y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E₂ : Type u_6<VAR>F : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E₂<VAR>Module R₂ E₂<VAR>NormedAddCommGroup F<VAR>Module R F<VAR>f₁ : F →ₛₗᵢ[σ₁₂] E₂<VAR>x y : F<VAR>h : x ≠ y<GOAL>f₁ x ≠ f₁ y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>LipschitzWith 1 ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>AntilipschitzWith 1 ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>Continuous ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<GOAL>⇑f ⁻¹' Metric.ball (f x) r = Metric.ball x r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<GOAL>⇑f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<GOAL>⇑f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>s : Set E<GOAL>EMetric.diam (⇑f '' s) = EMetric.diam s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>EMetric.diam (Set.range ⇑f) = EMetric.diam Set.univ
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>s : Set E<GOAL>Metric.diam (⇑f '' s) = Metric.diam s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<GOAL>Function.Injective LinearIsometry.toContinuousLinearMap
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f g : E →ₛₗᵢ[σ₁₂] E₂<GOAL>f.toContinuousLinearMap = g.toContinuousLinearMap ↔ f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>⇑f.toContinuousLinearMap = ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>α : Type u_11<VAR>TopologicalSpace α<VAR>g : α → E<GOAL>Continuous (⇑f ∘ g) ↔ Continuous g
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>⇑LinearIsometry.id = id
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>x : E<GOAL>LinearIsometry.id x = x
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>LinearIsometry.id.toLinearMap = LinearMap.id
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>LinearIsometry.id.toContinuousLinearMap = ContinuousLinearMap.id R E
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₁₃ : R →+* R₃<VAR>σ₂₃ : R₂ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>Module R E<VAR>Module R₂ E₂<VAR>Module R₃ E₃<VAR>g : E₂ →ₛₗᵢ[σ₂₃] E₃<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>LinearIsometry.id.comp f = f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<GOAL>f.comp LinearIsometry.id = f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>R₄ : Type u_4<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>E₄ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>Semiring R₄<VAR>σ₁₂ : R →+* R₂<VAR>σ₁₃ : R →+* R₃<VAR>σ₁₄ : R →+* R₄<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>SeminormedAddCommGroup E₄<VAR>Module R E<VAR>Module R₂ E₂<VAR>Module R₃ E₃<VAR>Module R₄ E₄<VAR>f : E₃ →ₛₗᵢ[σ₃₄] E₄<VAR>g : E₂ →ₛₗᵢ[σ₂₃] E₃<VAR>h : E →ₛₗᵢ[σ₁₂] E₂<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>⇑1 = id
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>f g : E →ₗᵢ[R] E<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>1 = LinearIsometry.id
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>f g : E →ₗᵢ[R] E<GOAL>f * g = f.comp g
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<VAR>f : E →ₗᵢ[R] E<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R' : Type u_11<VAR>Ring R'<VAR>Module R' E<VAR>p : Submodule R' E<GOAL>⇑p.subtypeₗᵢ = ⇑p.subtype
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R' : Type u_11<VAR>Ring R'<VAR>Module R' E<VAR>p : Submodule R' E<GOAL>p.subtypeₗᵢ.toLinearMap = p.subtype
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R' : Type u_11<VAR>Ring R'<VAR>Module R' E<VAR>p : Submodule R' E<GOAL>p.subtypeₗᵢ.toContinuousLinearMap = p.subtypeL
<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_11<VAR>E₂ : Type u_12<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>self : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<GOAL>‖self.toLinearEquiv x‖ = ‖x‖
<VAR>𝓕 : Type u_11<VAR>R : outParam (Type u_12)<VAR>R₂ : outParam (Type u_13)<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : outParam (R →+* R₂)<VAR>σ₂₁ : outParam (R₂ →+* R)<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>E : outParam (Type u_14)<VAR>E₂ : outParam (Type u_15)<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>EquivLike 𝓕 E E₂<VAR>self : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂<VAR>f : 𝓕<VAR>x : E<GOAL>‖f x‖ = ‖x‖