ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>f : E →ₛₗᵢ[σ₁₂] F<GOAL>‖f.toContinuousLinearMap‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>SeminormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>‖K.subtypeL‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CharZero 𝕜<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x : ↑(Metric.sphere 0 r)<GOAL>x ≠ -x
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CharZero 𝕜<VAR>x : ↑(Metric.sphere 0 1)<GOAL>x ≠ -x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<GOAL>balancedCore 𝕜 s ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<GOAL>balancedCore 𝕜 ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x : E<GOAL>x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<GOAL>a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<GOAL>Balanced 𝕜 (balancedCore 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s t : Set E<VAR>hs : Balanced 𝕜 s<VAR>h : s ⊆ t<GOAL>s ⊆ balancedCore 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x : E<GOAL>x ∈ balancedCoreAux 𝕜 s ↔ ∀ (r : 𝕜), 1 ≤ ‖r‖ → x ∈ r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x : E<GOAL>x ∈ balancedHull 𝕜 s ↔ ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s t : Set E<VAR>ht : Balanced 𝕜 t<VAR>h : s ⊆ t<GOAL>balancedHull 𝕜 s ⊆ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : 0 ∈ s<GOAL>0 ∈ balancedCore 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>(balancedCore 𝕜 s).Nonempty ↔ 0 ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormOneClass 𝕜<VAR>s : Set E<GOAL>s ⊆ balancedHull 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Balanced 𝕜 (balancedHull 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>balancedCoreAux 𝕜 ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>balancedCoreAux 𝕜 s ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h0 : 0 ∈ balancedCoreAux 𝕜 s<GOAL>Balanced 𝕜 (balancedCoreAux 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>h : t ⊆ s<VAR>ht : Balanced 𝕜 t<GOAL>t ⊆ balancedCoreAux 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>balancedCore 𝕜 s ⊆ balancedCoreAux 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : 0 ∈ s<GOAL>balancedCore 𝕜 s = ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>ht : 0 ∈ t<VAR>hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t<GOAL>s ⊆ balancedCore 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : IsClosed U<GOAL>IsClosed (balancedCore 𝕜 U)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<GOAL>balancedCore 𝕜 U ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<GOAL>(𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ Balanced 𝕜 s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>RegularSpace E<GOAL>(𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ IsClosed s ∧ Balanced 𝕜 s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Module ℝ E<VAR>SMulCommClass ℝ 𝕜 E<VAR>TopologicalSpace E<VAR>LocallyConvexSpace ℝ E<VAR>ContinuousSMul 𝕜 E<GOAL>(𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ Balanced 𝕜 s ∧ Convex ℝ s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Module ℝ E<VAR>SMulCommClass ℝ 𝕜 E<VAR>TopologicalSpace E<VAR>LocallyConvexSpace ℝ E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousSMul ℝ E<VAR>TopologicalAddGroup E<GOAL>(𝓝 0).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Zero E<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>SMul ℝ E<VAR>s : AbsConvexOpenSets 𝕜 E<GOAL>0 ∈ ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Zero E<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>SMul ℝ E<VAR>s : AbsConvexOpenSets 𝕜 E<GOAL>IsOpen ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Zero E<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>SMul ℝ E<VAR>s : AbsConvexOpenSets 𝕜 E<GOAL>↑s ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Zero E<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>SMul ℝ E<VAR>s : AbsConvexOpenSets 𝕜 E<GOAL>Balanced 𝕜 ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Zero E<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>SMul ℝ E<VAR>s : AbsConvexOpenSets 𝕜 E<GOAL>Convex ℝ ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>Module ℝ E<VAR>IsScalarTower ℝ 𝕜 E<VAR>ContinuousSMul ℝ E<VAR>s : AbsConvexOpenSets 𝕜 E<GOAL>(gaugeSeminormFamily 𝕜 E s).ball 0 1 = ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>Module ℝ E<VAR>IsScalarTower ℝ 𝕜 E<VAR>ContinuousSMul ℝ E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>SMulCommClass ℝ 𝕜 E<VAR>LocallyConvexSpace ℝ E<GOAL>WithSeminorms (gaugeSeminormFamily 𝕜 E)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E →ₗ[𝕜] 𝕜<GOAL>⇑f.toSeminorm = fun x => ‖f x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E →ₗ[𝕜] 𝕜<VAR>x : E<GOAL>f.toSeminorm x = ‖f x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E →ₗ[𝕜] 𝕜<VAR>r : ℝ<GOAL>f.toSeminorm.ball 0 r = {x | ‖f x‖ < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>f : F →ₗ[𝕜] 𝕜<VAR>g : E →ₗ[𝕜] F<GOAL>f.toSeminorm.comp g = (f ∘ₗ g).toSeminorm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>x : E<VAR>y : F<GOAL>(B.toSeminormFamily y) x = ‖(B x) y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<GOAL>(𝓝 0).HasBasis B.toSeminormFamily.basisSets id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<GOAL>WithSeminorms B.toSeminormFamily
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>y : F<GOAL>y ∈ B.polar s ↔ ∀ x ∈ s, ‖(B x) y‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>y : F<VAR>hy : y ∈ B.polar s<VAR>x : E<GOAL>x ∈ s → ‖(B x) y‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<GOAL>0 ∈ B.polar s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<GOAL>B.polar s = ⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ B.polar) (B.flip.polar ∘ ⇑OrderDual.ofDual)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>ι : Sort u_4<VAR>s : ι → Set E<GOAL>B.polar (⋃ i, s i) = ⋂ i, B.polar (s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s t : Set E<GOAL>B.polar (s ∪ t) = B.polar s ∩ B.polar t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<GOAL>Antitone B.polar
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<GOAL>B.polar ∅ = Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<GOAL>B.polar {0} = Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<GOAL>s ⊆ B.flip.polar (B.polar s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<GOAL>B.polar (B.flip.polar (B.polar s)) = B.polar s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedCommRing 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<GOAL>IsClosed (B.polar s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>h : B.SeparatingRight<GOAL>B.polar Set.univ = {0}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>S : Type u_4<VAR>SetLike S E<VAR>SMulMemClass S 𝕜 E<VAR>m : S<GOAL>B.polar ↑m = {y | ∀ x ∈ m, (B x) y = 0}
<VAR>x₀ : ℝ<VAR>a : ℕ<VAR>f : ℝ → ℝ<VAR>hf : AntitoneOn f (Set.Icc x₀ (x₀ + ↑a))<GOAL>∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑i)
<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Set.Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ x ∈ Finset.Ico a b, f ↑x
<VAR>x₀ : ℝ<VAR>a : ℕ<VAR>f : ℝ → ℝ<VAR>hf : AntitoneOn f (Set.Icc x₀ (x₀ + ↑a))<GOAL>∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Set.Icc ↑a ↑b)<GOAL>∑ i ∈ Finset.Ico a b, f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, f x
<VAR>x₀ : ℝ<VAR>a : ℕ<VAR>f : ℝ → ℝ<VAR>hf : MonotoneOn f (Set.Icc x₀ (x₀ + ↑a))<GOAL>∑ i ∈ Finset.range a, f (x₀ + ↑i) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : MonotoneOn f (Set.Icc ↑a ↑b)<GOAL>∑ x ∈ Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x
<VAR>x₀ : ℝ<VAR>a : ℕ<VAR>f : ℝ → ℝ<VAR>hf : MonotoneOn f (Set.Icc x₀ (x₀ + ↑a))<GOAL>∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1))
<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : MonotoneOn f (Set.Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ i ∈ Finset.Ico a b, f ↑(i + 1)
<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>f : P →ᵃⁱ[𝕜] P₂<GOAL>f.linear = f.linearIsometry.toLinearMap
<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₂<GOAL>⇑f.toAffineMap = ⇑f
<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 AffineIsometry.toAffineMap
<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 DFunLike.coe
<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 g : P →ᵃⁱ[𝕜] P₂<VAR>h : ∀ (x : P), f x = g x<GOAL>f = g
<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>f : V →ₗᵢ[𝕜] V₂<GOAL>⇑f.toAffineIsometry = ⇑f
<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>f : V →ₗᵢ[𝕜] V₂<GOAL>f.toAffineIsometry.linearIsometry = f
<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>f : V →ₗᵢ[𝕜] V₂<GOAL>f.toAffineIsometry.toAffineMap = f.toAffineMap
<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>p : P<VAR>v : V<GOAL>f (v +ᵥ p) = f.linearIsometry v +ᵥ f 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>p1 p2 : P<GOAL>f.linearIsometry (p1 -ᵥ p2) = f p1 -ᵥ f 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>f : P →ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>dist (f x) (f 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>f : P →ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>nndist (f x) (f y) = nndist 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>f : P →ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>edist (f x) (f 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>f : P →ᵃⁱ[𝕜] P₂<GOAL>Isometry ⇑f
<VAR>𝕜 : Type u_1<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>P₁' : Type u_9<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V₁'<VAR>NormedSpace 𝕜 V₁'<VAR>MetricSpace P₁'<VAR>NormedAddTorsor V₁' P₁'<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>f₁ : P₁' →ᵃⁱ[𝕜] P₂<GOAL>Function.Injective ⇑f₁
<VAR>𝕜 : Type u_1<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>P₁' : Type u_9<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V₁'<VAR>NormedSpace 𝕜 V₁'<VAR>MetricSpace P₁'<VAR>NormedAddTorsor V₁' P₁'<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>f₁ : P₁' →ᵃⁱ[𝕜] P₂<VAR>x y : P₁'<GOAL>f₁ x = f₁ y ↔ x = y
<VAR>𝕜 : Type u_1<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>P₁' : Type u_9<VAR>P₂ : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V₁'<VAR>NormedSpace 𝕜 V₁'<VAR>MetricSpace P₁'<VAR>NormedAddTorsor V₁' P₁'<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₂<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>f₁ : P₁' →ᵃⁱ[𝕜] P₂<VAR>x y : P₁'<VAR>h : x ≠ y<GOAL>f₁ x ≠ f₁ 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>f : P →ᵃⁱ[𝕜] P₂<GOAL>LipschitzWith 1 ⇑f
<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₂<GOAL>AntilipschitzWith 1 ⇑f
<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₂<GOAL>Continuous ⇑f
<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>s : Set P<GOAL>EMetric.diam (⇑f '' 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>f : P →ᵃⁱ[𝕜] P₂<GOAL>EMetric.diam (Set.range ⇑f) = EMetric.diam 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>f : P →ᵃⁱ[𝕜] P₂<VAR>s : Set P<GOAL>Metric.diam (⇑f '' 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>f : P →ᵃⁱ[𝕜] P₂<GOAL>Metric.diam (Set.range ⇑f) = Metric.diam 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>f : P →ᵃⁱ[𝕜] P₂<VAR>α : Type u_14<VAR>TopologicalSpace α<VAR>g : α → P<GOAL>Continuous (⇑f ∘ g) ↔ Continuous 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<GOAL>⇑AffineIsometry.id = 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>x : P<GOAL>AffineIsometry.id x = 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>AffineIsometry.id.toAffineMap = AffineMap.id 𝕜 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>g : P₂ →ᵃⁱ[𝕜] P₃<VAR>f : P →ᵃⁱ[𝕜] P₂<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<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₂<GOAL>AffineIsometry.id.comp f = f
<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₂<GOAL>f.comp AffineIsometry.id = f
<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>f : P₃ →ᵃⁱ[𝕜] P₄<VAR>g : P₂ →ᵃⁱ[𝕜] P₃<VAR>h : P →ᵃⁱ[𝕜] P₂<GOAL>(f.comp g).comp h = f.comp (g.comp h)