ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(s.sup p).closedBall x r = s.inf fun i => (p i).closedBall x r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>p.ball x r = ∅
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : r < 0<GOAL>p.closedBall x r = ∅
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r₁ : ℝ<VAR>hr₁ : r₁ ≠ 0<VAR>r₂ : ℝ<GOAL>Metric.closedBall 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r₁ : ℝ<VAR>r₂ : ℝ<VAR>hr₂ : r₂ ≠ 0<GOAL>Metric.ball 0 r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<GOAL>Metric.ball 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<GOAL>Metric.closedBall 0 r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>x : E<GOAL>-x ∈ p.ball 0 r ↔ x ∈ p.ball 0 r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>x : E<GOAL>-p.ball x r = p.ball (-x) r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (Set.range p)<VAR>e : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<GOAL>p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : k ≠ 0<GOAL>k • p.ball 0 r = p.ball 0 (‖k‖ * r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<GOAL>k • p.closedBall 0 r ⊆ p.closedBall 0 (‖k‖ * r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : 0 < ‖k‖<GOAL>k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₁ : 0 < r₁<GOAL>Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Absorbent 𝕜 (p.ball 0 r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Absorbent 𝕜 (p.closedBall 0 r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hpr : p x < r<GOAL>Absorbent 𝕜 (p.ball x r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hpr : p x < r<GOAL>Absorbent 𝕜 (p.closedBall x r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>y : E<VAR>r : ℝ<VAR>a : 𝕜<VAR>ha : a ≠ 0<GOAL>(fun x => a • x) ⁻¹' p.ball y r = p.ball (a⁻¹ • y) (r / ‖a‖)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>NormedSpace ℝ 𝕜<VAR>Module 𝕜 E<VAR>SMul ℝ E<VAR>IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<GOAL>ConvexOn ℝ Set.univ ⇑p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>NormedSpace ℝ 𝕜<VAR>Module 𝕜 E<VAR>Module ℝ E<VAR>IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>Convex ℝ (p.ball x r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>NormedSpace ℝ 𝕜<VAR>Module 𝕜 E<VAR>Module ℝ E<VAR>IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>Convex ℝ (p.closedBall x r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>𝕜' : Type u_13<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormOneClass 𝕜'<VAR>AddCommGroup E<VAR>Module 𝕜' E<VAR>SMul 𝕜 E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>p : Seminorm 𝕜' E<GOAL>⇑(Seminorm.restrictScalars 𝕜 p) = ⇑p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>𝕜' : Type u_13<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormOneClass 𝕜'<VAR>AddCommGroup E<VAR>Module 𝕜' E<VAR>SMul 𝕜 E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>p : Seminorm 𝕜' E<GOAL>(Seminorm.restrictScalars 𝕜 p).ball = p.ball
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>𝕜' : Type u_13<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormOneClass 𝕜'<VAR>AddCommGroup E<VAR>Module 𝕜' E<VAR>SMul 𝕜 E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>p : Seminorm 𝕜' E<GOAL>(Seminorm.restrictScalars 𝕜 p).closedBall = p.closedBall
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>TopologicalSpace E<VAR>p : Seminorm 𝕝 E<VAR>hp : ∀ r > 0, p.closedBall 0 r ∈ 𝓝 0<GOAL>ContinuousAt (⇑p) 0
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.closedBall 0 r ∈ 𝓝 0<GOAL>ContinuousAt (⇑p) 0
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>TopologicalSpace E<VAR>p : Seminorm 𝕝 E<VAR>hp : ∀ r > 0, p.ball 0 r ∈ 𝓝 0<GOAL>ContinuousAt (⇑p) 0
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.ball 0 r ∈ 𝓝 0<GOAL>ContinuousAt (⇑p) 0
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ContinuousAt (⇑p) 0<GOAL>UniformContinuous ⇑p
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ContinuousAt (⇑p) 0<GOAL>Continuous ⇑p
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ∀ r > 0, p.ball 0 r ∈ 𝓝 0<GOAL>UniformContinuous ⇑p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.ball 0 r ∈ 𝓝 0<GOAL>UniformContinuous ⇑p
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ∀ r > 0, p.closedBall 0 r ∈ 𝓝 0<GOAL>UniformContinuous ⇑p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.closedBall 0 r ∈ 𝓝 0<GOAL>UniformContinuous ⇑p
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ∀ r > 0, p.ball 0 r ∈ 𝓝 0<GOAL>Continuous ⇑p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.ball 0 r ∈ 𝓝 0<GOAL>Continuous ⇑p
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ∀ r > 0, p.closedBall 0 r ∈ 𝓝 0<GOAL>Continuous ⇑p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.closedBall 0 r ∈ 𝓝 0<GOAL>Continuous ⇑p
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>p q : Seminorm 𝕝 E<VAR>hq : Continuous ⇑q<VAR>hpq : p ≤ q<GOAL>Continuous ⇑p
<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>SeminormedRing 𝕝<VAR>AddCommGroup E<VAR>Module 𝕝 E<VAR>TopologicalSpace E<VAR>p : Seminorm 𝕝 E<VAR>hp : Continuous ⇑p<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>p.ball 0 r ∈ 𝓝 0
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ι : Sort u_13<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>p' : ι → Prop<VAR>s : ι → Set E<VAR>p : Seminorm 𝕜 E<VAR>hb : (𝓝 0).HasBasis p' s<VAR>h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0<VAR>h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i<GOAL>inst✝ = PseudoMetricSpace.toUniformSpace
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ι : Sort u_13<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>p' : ι → Prop<VAR>s : ι → Set E<VAR>p : Seminorm 𝕜 E<VAR>hb : (𝓝 0).HasBasis p' s<VAR>h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0<VAR>h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i<GOAL>𝓤 E = ⨅ r, ⨅ (_ : r > 0), 𝓟 {x | p (x.1 - x.2) < r}
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>x : E<VAR>hx : p x ≠ 0<GOAL>∃ n, c ^ n ≠ 0 ∧ p (c ^ n • x) < ε ∧ ε / ‖c‖ ≤ p (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>x : E<VAR>hx : p x ≠ 0<GOAL>∃ d, d ≠ 0 ∧ p (d • x) < ε ∧ ε / ‖c‖ ≤ p (d • x) ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x<VAR>x : E<VAR>hx : p x ≠ 0<GOAL>q x ≤ C * p x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>ε : ℝ<VAR>C : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ (C • p) x<VAR>x : E<VAR>hx : p x ≠ 0<GOAL>q x ≤ (C • p) x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>q : Seminorm 𝕜 E<VAR>ε : ℝ<VAR>C : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x<VAR>x : E<VAR>hx : ∃ j ∈ s, (p j) x ≠ 0<GOAL>q x ≤ (C • s.sup p) x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Set E<VAR>hs : Absorbent 𝕜 s<VAR>h : ∀ x ∈ s, BddAbove (Set.range fun x_1 => (p x_1) x)<GOAL>BddAbove (Set.range p)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>⇑(normSeminorm 𝕜 E) = norm
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>(normSeminorm 𝕜 E).ball = Metric.ball
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Absorbent 𝕜 (Metric.ball 0 r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hx : ‖x‖ < r<GOAL>Absorbent 𝕜 (Metric.ball x r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<GOAL>Balanced 𝕜 (Metric.ball 0 r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<GOAL>∃ n, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<GOAL>∃ d, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
<VAR>𝕜 : Type u_3<VAR>F : Type u_10<VAR>NormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>x : F<VAR>hx : x ≠ 0<GOAL>∃ n, c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
<VAR>𝕜 : Type u_3<VAR>F : Type u_10<VAR>NormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>x : F<VAR>hx : x ≠ 0<GOAL>∃ d, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LE β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<GOAL>QuasiconvexOn 𝕜 s f → QuasiconcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LE β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<GOAL>QuasiconcaveOn 𝕜 s f → QuasiconvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LE β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<GOAL>QuasilinearOn 𝕜 s f → QuasilinearOn 𝕜 s (⇑OrderDual.toDual ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LE β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hs : Convex 𝕜 s<VAR>h : ∀ (r : β), Convex 𝕜 {x | f x ≤ r}<GOAL>QuasiconvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LE β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hs : Convex 𝕜 s<VAR>h : ∀ (r : β), Convex 𝕜 {x | r ≤ f x}<GOAL>QuasiconcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LE β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>IsDirected β fun x x_1 => x ≤ x_1<VAR>hf : QuasiconvexOn 𝕜 s f<GOAL>Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LE β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>IsDirected β fun x x_1 => x ≥ x_1<VAR>hf : QuasiconcaveOn 𝕜 s f<GOAL>Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<VAR>SemilatticeSup β<VAR>hf : QuasiconvexOn 𝕜 s f<VAR>hg : QuasiconvexOn 𝕜 s g<GOAL>QuasiconvexOn 𝕜 s (f ⊔ g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<VAR>SemilatticeInf β<VAR>hf : QuasiconcaveOn 𝕜 s f<VAR>hg : QuasiconcaveOn 𝕜 s g<GOAL>QuasiconcaveOn 𝕜 s (f ⊓ g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrder β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<GOAL>QuasiconvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrder β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<GOAL>QuasiconcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrder β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<GOAL>QuasilinearOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ Set.uIcc (f x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrder β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : QuasiconvexOn 𝕜 s f<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ f x < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>LinearOrder β<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : QuasiconcaveOn 𝕜 s f<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ r < f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<GOAL>QuasiconvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConcaveOn 𝕜 s f<GOAL>QuasiconcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : MonotoneOn f s<VAR>hs : Convex 𝕜 s<GOAL>QuasiconvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : MonotoneOn f s<VAR>hs : Convex 𝕜 s<GOAL>QuasiconcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : MonotoneOn f s<VAR>hs : Convex 𝕜 s<GOAL>QuasilinearOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : AntitoneOn f s<VAR>hs : Convex 𝕜 s<GOAL>QuasiconvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : AntitoneOn f s<VAR>hs : Convex 𝕜 s<GOAL>QuasiconcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : AntitoneOn f s<VAR>hs : Convex 𝕜 s<GOAL>QuasilinearOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Monotone f<GOAL>QuasiconvexOn 𝕜 Set.univ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Monotone f<GOAL>QuasiconcaveOn 𝕜 Set.univ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Monotone f<GOAL>QuasilinearOn 𝕜 Set.univ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Antitone f<GOAL>QuasiconvexOn 𝕜 Set.univ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Antitone f<GOAL>QuasiconcaveOn 𝕜 Set.univ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Antitone f<GOAL>QuasilinearOn 𝕜 Set.univ f
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>LinearOrder β<VAR>hf : QuasilinearOn 𝕜 s f<GOAL>MonotoneOn f s ∨ AntitoneOn f s
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>LinearOrderedAddCommMonoid β<VAR>hs : Convex 𝕜 s<GOAL>QuasilinearOn 𝕜 s f ↔ MonotoneOn f s ∨ AntitoneOn f s
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace A<VAR>T2Space A<VAR>Ring A<VAR>StarRing A<VAR>Algebra 𝕜 A<VAR>h : ∀ (a : A), CompactSpace ↑(spectrum 𝕜 a)<GOAL>UniqueContinuousFunctionalCalculus 𝕜 A
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Continuous ContinuousMap.toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : C(X, ℝ)<VAR>x : X<GOAL>f.toNNReal x = (f x).toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f g : C(X, ℝ)<GOAL>(f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f g : C(X, ℝ)<GOAL>(f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal = (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>r : NNReal<GOAL>((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = (algebraMap NNReal C(X, NNReal)) r
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>r : NNReal<GOAL>(-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = 0
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>ContinuousMap.toNNReal 1 = 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>(-1).toNNReal = 0
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A : Type u_2<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℝ A<VAR>φ : C(X, NNReal) →⋆ₐ[NNReal] A<VAR>f : C(X, ℝ)<GOAL>φ.realContinuousMapOfNNReal f = φ f.toNNReal - φ (-f).toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A : Type u_2<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℝ A<VAR>TopologicalRing A<VAR>φ : C(X, NNReal) →⋆ₐ[NNReal] A<VAR>hφ : Continuous ⇑φ<GOAL>Continuous ⇑φ.realContinuousMapOfNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A : Type u_2<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℝ A<VAR>φ : C(X, NNReal) →⋆ₐ[NNReal] A<VAR>f : C(X, NNReal)<GOAL>φ.realContinuousMapOfNNReal ({ toFun := NNReal.toReal, continuous_toFun := NNReal.continuous_coe }.comp f) = φ f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>A : Type u_2<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℝ A<GOAL>Function.Injective StarAlgHom.realContinuousMapOfNNReal
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace A<VAR>T2Space A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>h : ∀ (a : A), CompactSpace ↑(quasispectrum 𝕜 a)<GOAL>UniqueNonUnitalContinuousFunctionalCalculus 𝕜 A
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>f : ContinuousMapZero X ℝ<VAR>x : X<GOAL>f.toNNReal x = (f x).toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<GOAL>Continuous ContinuousMapZero.toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>f : ContinuousMapZero X ℝ<GOAL>(ContinuousMapZero.toContinuousMapHom f).toNNReal = ContinuousMapZero.toContinuousMapHom f.toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>r : NNReal<VAR>f : ContinuousMapZero X ℝ<GOAL>(r • f).toNNReal = r • f.toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>r : NNReal<VAR>f : ContinuousMapZero X ℝ<GOAL>(-(r • f)).toNNReal = r • (-f).toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>f g : ContinuousMapZero X ℝ<GOAL>(f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal = (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>f g : ContinuousMapZero X ℝ<GOAL>(f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Zero X<VAR>A : Type u_2<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module ℝ A<VAR>φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A<VAR>f : ContinuousMapZero X ℝ<GOAL>φ.realContinuousMapZeroOfNNReal f = φ f.toNNReal - φ (-f).toNNReal