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<VAR>x : P<GOAL>(AffineIsometryEquiv.pointReflection 𝕜 x) 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<VAR>x : P<GOAL>Function.Involutive ⇑(AffineIsometryEquiv.pointReflection 𝕜 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).symm = AffineIsometryEquiv.pointReflection 𝕜 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 y : P<GOAL>dist ((AffineIsometryEquiv.pointReflection 𝕜 x) y) x = dist 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 y : P<GOAL>dist ((AffineIsometryEquiv.pointReflection 𝕜 x) y) y = ‖2 • (x -ᵥ y)‖
<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>dist ((AffineIsometryEquiv.pointReflection 𝕜 x) y) y = ‖2‖ * dist x y
<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>Invertible 2<VAR>x y : P<GOAL>(AffineIsometryEquiv.pointReflection 𝕜 x) y = y ↔ y = x
<VAR>V : Type u_2<VAR>P : Type u_10<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedSpace ℝ V<VAR>x y : P<GOAL>dist ((AffineIsometryEquiv.pointReflection ℝ x) y) y = 2 * dist x y
<VAR>V : Type u_2<VAR>P : Type u_10<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedSpace ℝ V<VAR>x y : P<GOAL>(AffineIsometryEquiv.pointReflection ℝ (midpoint ℝ x y)) x = y
<VAR>V : Type u_2<VAR>P : Type u_10<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedSpace ℝ V<VAR>x y : P<GOAL>(AffineIsometryEquiv.pointReflection ℝ (midpoint ℝ x y)) y = 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>Continuous ⇑f.linear ↔ 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₂<GOAL>IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f
<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 : AffineSubspace 𝕜 P₁<VAR>Nonempty ↥E<VAR>φ : P₁ →ᵃ[𝕜] P₂<VAR>hφ : Function.Injective ⇑φ<GOAL>(E.equivMapOfInjective φ hφ).linear = (Submodule.equivMapOfInjective φ.linear ⋯ E.direction).trans (LinearEquiv.ofEq (Submodule.map φ.linear E.direction) (AffineSubspace.map φ E).direction ⋯)
<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 : AffineSubspace 𝕜 P₁<VAR>Nonempty ↥E<VAR>φ : P₁ →ᵃ[𝕜] P₂<VAR>hφ : Function.Injective ⇑φ<VAR>p : ↑↑E<GOAL>(E.equivMapOfInjective φ hφ) p = ⟨φ ↑p, ⋯⟩
<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>E : AffineSubspace 𝕜 P₁'<VAR>Nonempty ↥E<VAR>φ : P₁' →ᵃⁱ[𝕜] P₂<VAR>x : ↥(AffineSubspace.map φ.toAffineMap E)<GOAL>φ ↑((AffineSubspace.isometryEquivMap φ E).symm x) = ↑x
<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>φ : P₁' →ᵃⁱ[𝕜] P₂<VAR>E : AffineSubspace 𝕜 P₁'<VAR>Nonempty ↥E<VAR>g : ↥E<GOAL>↑((AffineSubspace.isometryEquivMap φ E) g) = φ ↑g
<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>φ : P₁' →ᵃⁱ[𝕜] P₂<VAR>E : AffineSubspace 𝕜 P₁'<VAR>Nonempty ↥E<GOAL>↑(AffineSubspace.isometryEquivMap φ E).toAffineEquiv = ↑(E.equivMapOfInjective φ.toAffineMap ⋯)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedAddCommGroup 𝕜<VAR>SeminormedAddCommGroup E<VAR>SMulZeroClass 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<GOAL>EMetric.diam (c • s) ≤ ‖c‖₊ • EMetric.diam s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<GOAL>EMetric.diam (c • s) = ‖c‖₊ • EMetric.diam s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>x : Set E<GOAL>Metric.diam (c • x) = ‖c‖ * Metric.diam x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>s : Set E<VAR>x : E<GOAL>EMetric.infEdist (c • x) (c • s) = ‖c‖₊ • EMetric.infEdist x s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>s : Set E<VAR>x : E<GOAL>Metric.infDist (c • x) (c • s) = ‖c‖ * Metric.infDist x s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<GOAL>c • Metric.ball x r = Metric.ball (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>c • Metric.ball 0 1 = Metric.ball 0 ‖c‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<GOAL>c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<GOAL>c • Metric.closedBall x r = Metric.closedBall (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set 𝕜<VAR>hs : 0 ∉ s<VAR>r : ℝ<GOAL>s • Metric.sphere 0 r = (fun x => ‖x‖) ⁻¹' ((fun x => ‖x‖ * r) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>c : 𝕜<GOAL>Bornology.IsBounded (c • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<GOAL>∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>r • Metric.ball 0 1 = Metric.ball 0 r
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b r : ℝ<VAR>ha : 0 ≤ a<VAR>hr : 0 < r<GOAL>Set.Ioo a b • Metric.sphere 0 r = Metric.ball 0 (b * r) \ Metric.closedBall 0 (a * r)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x z : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : dist x z ≤ ε + δ<GOAL>∃ y, dist x y ≤ δ ∧ dist y z ≤ ε
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 < ε<VAR>h : dist x z < ε + δ<GOAL>∃ y, dist x y ≤ δ ∧ dist y z < ε
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<VAR>h : dist x z < ε + δ<GOAL>∃ y, dist x y < δ ∧ dist y z ≤ ε
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : dist x z < ε + δ<GOAL>∃ y, dist x y < δ ∧ dist y z < ε
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x y : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<GOAL>Disjoint (Metric.ball x δ) (Metric.ball y ε) ↔ δ + ε ≤ dist x y
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x y : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<GOAL>Disjoint (Metric.ball x δ) (Metric.closedBall y ε) ↔ δ + ε ≤ dist x y
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x y : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 < ε<GOAL>Disjoint (Metric.closedBall x δ) (Metric.ball y ε) ↔ δ + ε ≤ dist x y
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x y : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<GOAL>Disjoint (Metric.closedBall x δ) (Metric.closedBall y ε) ↔ δ + ε < dist x y
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<GOAL>EMetric.infEdist x (Metric.thickening δ s) = EMetric.infEdist x s - ENNReal.ofReal δ
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>s : Set E<GOAL>Metric.thickening ε (Metric.thickening δ s) = Metric.thickening (ε + δ) s
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 < δ<VAR>s : Set E<GOAL>Metric.cthickening ε (Metric.thickening δ s) = Metric.cthickening (ε + δ) s
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<GOAL>closure (Metric.thickening δ s) = Metric.cthickening δ s
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>EMetric.infEdist x (Metric.cthickening δ s) = EMetric.infEdist x s - ENNReal.ofReal δ
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 ≤ δ<VAR>s : Set E<GOAL>Metric.thickening ε (Metric.cthickening δ s) = Metric.thickening (ε + δ) s
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>s : Set E<GOAL>Metric.cthickening ε (Metric.cthickening δ s) = Metric.cthickening (ε + δ) s
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>x : E<GOAL>Metric.thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>Metric.thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 < δ<VAR>x : E<GOAL>Metric.cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>Metric.cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>a b : E<GOAL>Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>a b : E<GOAL>Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 ≤ δ<VAR>a b : E<GOAL>Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 ≤ δ<VAR>a b : E<GOAL>Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 < δ<VAR>a b : E<GOAL>Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 < δ<VAR>a b : E<GOAL>Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>ProperSpace E<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>a b : E<GOAL>Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>δ ε : ℝ<VAR>ProperSpace E<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>a b : E<GOAL>Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>c • Metric.closedBall x r = Metric.closedBall (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<GOAL>c • Metric.closedBall 0 1 = Metric.closedBall 0 ‖c‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>r • Metric.closedBall 0 1 = Metric.closedBall 0 r
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>(Metric.sphere x r).Nonempty ↔ 0 ≤ r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<VAR>c : 𝕜<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>c • Metric.sphere x r = Metric.sphere (c • x) (‖c‖ * r)
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : E<GOAL>x +ᵥ r • Metric.ball 0 1 = Metric.ball x r
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x : E<GOAL>x +ᵥ r • Metric.closedBall 0 1 = Metric.closedBall x r
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>A B : Set E<GOAL>Absorbs 𝕜 A B ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>A B : Set E<VAR>h : Absorbs 𝕜 A B<GOAL>∃ r > 0, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<GOAL>Balanced 𝕜 s ↔ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<GOAL>Balanced 𝕜 s ↔ Metric.closedBall 0 1 • s ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<GOAL>Balanced 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<GOAL>Balanced 𝕜 Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>A B : Set E<VAR>hA : Balanced 𝕜 A<VAR>hB : Balanced 𝕜 B<GOAL>Balanced 𝕜 (A ∪ B)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>A B : Set E<VAR>hA : Balanced 𝕜 A<VAR>hB : Balanced 𝕜 B<GOAL>Balanced 𝕜 (A ∩ B)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>f : ι → Set E<VAR>h : ∀ (i : ι), Balanced 𝕜 (f i)<GOAL>Balanced 𝕜 (⋃ i, f i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>f : (i : ι) → κ i → Set E<VAR>h : ∀ (i : ι) (j : κ i), Balanced 𝕜 (f i j)<GOAL>Balanced 𝕜 (⋃ i, ⋃ j, f i j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>f : ι → Set E<VAR>h : ∀ (i : ι), Balanced 𝕜 (f i)<GOAL>Balanced 𝕜 (⋂ i, f i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>f : (i : ι) → κ i → Set E<VAR>h : ∀ (i : ι) (j : κ i), Balanced 𝕜 (f i j)<GOAL>Balanced 𝕜 (⋂ i, ⋂ j, f i j)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>SMul 𝕝 E<VAR>SMulCommClass 𝕜 𝕝 E<VAR>a : 𝕝<VAR>hs : Balanced 𝕜 s<GOAL>Balanced 𝕜 (a • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Balanced 𝕜 s → Balanced 𝕜 (-s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Balanced 𝕜 (-s) ↔ Balanced 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>NormOneClass 𝕜<VAR>h : Balanced 𝕜 s<VAR>x : E<GOAL>-x ∈ s ↔ x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>NormOneClass 𝕜<VAR>h : Balanced 𝕜 s<GOAL>-s = s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hs : Balanced 𝕜 s<VAR>ht : Balanced 𝕜 t<GOAL>Balanced 𝕜 (s + t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hs : Balanced 𝕜 s<VAR>ht : Balanced 𝕜 t<GOAL>Balanced 𝕜 (s - t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>Balanced 𝕜 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedDivisionRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<GOAL>Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, Set.MapsTo (fun x => c • x) t s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedDivisionRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Absorbent 𝕜 s ↔ ∀ (x : E), ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, c • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedDivisionRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>h₀ : 0 ∈ s<GOAL>Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝 0, Set.MapsTo (fun x => c • x) t s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedDivisionRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>h : Absorbs 𝕜 s t<VAR>h₀ : 0 ∈ s<GOAL>∀ᶠ (c : 𝕜) in 𝓝 0, Set.MapsTo (fun x => c • x) t s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>NormedRing 𝕝<VAR>NormedSpace 𝕜 𝕝<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>SMulWithZero 𝕝 E<VAR>IsScalarTower 𝕜 𝕝 E<VAR>s : Set E<VAR>hs : Balanced 𝕝 s<VAR>a : 𝕝<VAR>b : 𝕜<VAR>h : ‖a‖ ≤ ‖b‖<GOAL>a • s ⊆ b • s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>NormedRing 𝕝<VAR>NormedSpace 𝕜 𝕝<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>SMulWithZero 𝕝 E<VAR>IsScalarTower 𝕜 𝕝 E<VAR>s : Set E<VAR>x : E<VAR>SMulCommClass 𝕝 𝕜 E<VAR>hs : Balanced 𝕝 s<VAR>a : 𝕜<VAR>b : 𝕝<VAR>ha : a • x ∈ s<VAR>hba : ‖b‖ ≤ ‖a‖<GOAL>b • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>a : 𝕜<VAR>hA : Balanced 𝕜 A<VAR>ha : 1 ≤ ‖a‖<GOAL>A ⊆ a • A
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>a b : 𝕜<VAR>hs : Balanced 𝕜 A<VAR>h : ‖a‖ = ‖b‖<GOAL>a • A = b • A
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>a : 𝕜<VAR>hA : Balanced 𝕜 A<VAR>ha : ‖a‖ = 1<GOAL>a • A = A
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>hA : Balanced 𝕜 A<GOAL>Absorbs 𝕜 A A
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>a b : 𝕜<VAR>hs : Balanced 𝕜 s<VAR>h : ‖a‖ = ‖b‖<GOAL>a • x ∈ s ↔ b • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>hA : A ∈ 𝓝 0<GOAL>Absorbent 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<GOAL>Balanced 𝕜 (insert 0 (interior A))
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<GOAL>Balanced 𝕜 (0 ∪ interior A)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<VAR>h : 0 ∈ interior A<GOAL>Balanced 𝕜 (interior A)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<GOAL>Balanced 𝕜 (closure A)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Absorbent 𝕜 s<GOAL>0 ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>Module ℝ E<VAR>SMulCommClass ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<GOAL>Balanced 𝕜 ((convexHull ℝ) s)
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<GOAL>Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
<VAR>f : C(ℝ, ℂ)<VAR>hf : ∀ (K : TopologicalSpace.Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>m : ℤ<GOAL>fourierCoeff ⋯.lift m = 𝓕 ⇑f ↑m
<VAR>f : C(ℝ, ℂ)<VAR>h_norm : ∀ (K : TopologicalSpace.Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>h_sum : Summable fun n => 𝓕 ⇑f ↑n<VAR>x : ℝ<GOAL>∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[Filter.atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<GOAL>(fun x => ‖ContinuousMap.restrict (Set.Icc (x + R) (x + S)) f‖) =O[Filter.atTop] fun x => |x| ^ (-b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[Filter.atBot] fun x => |x| ^ (-b)<VAR>R S : ℝ<GOAL>(fun x => ‖ContinuousMap.restrict (Set.Icc (x + R) (x + S)) f‖) =O[Filter.atBot] fun x => |x| ^ (-b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)<VAR>K : TopologicalSpace.Compacts ℝ<GOAL>(fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)
<VAR>f : ℝ → ℂ<VAR>hc : Continuous f<VAR>b : ℝ<VAR>hb : 1 < b<VAR>hf : f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)<VAR>hFf : Summable fun n => 𝓕 f ↑n<VAR>x : ℝ<GOAL>∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 f ↑n * (fourier n) ↑x
<VAR>f : ℝ → ℂ<VAR>hc : Continuous f<VAR>b : ℝ<VAR>hb : 1 < b<VAR>hf : f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)<VAR>hFf : 𝓕 f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)<VAR>x : ℝ<GOAL>∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 f ↑n * (fourier n) ↑x
<VAR>f g : SchwartzMap ℝ ℂ<VAR>hfg : 𝓕 ⇑f = ⇑g<VAR>x : ℝ<GOAL>∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), g ↑n * (fourier n) ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<GOAL>Bornology.IsVonNBounded 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ ∀ V ∈ 𝓝 0, Absorbs 𝕜 V s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_6<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>q : ι → Prop<VAR>s : ι → Set E<VAR>A : Set E<VAR>h : (𝓝 0).HasBasis q s<GOAL>Bornology.IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A