ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>a : ℝ<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : Absorbent ℝ s<VAR>ha : 0 ≤ a<GOAL>{x | gauge s x ≤ a} = ⋂ r, ⋂ (_ : a < r), r • s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>absorbs : Absorbent ℝ s<VAR>a : ℝ<GOAL>{x | gauge s x < a} = ⋃ r, ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>absorbs : Absorbent ℝ s<VAR>a : ℝ<GOAL>{x | gauge s x < a} = ⋃ r ∈ Set.Ioo 0 a, r • s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>absorbs : Absorbent ℝ s<VAR>hgauge : gauge s x < 1<GOAL>∃ y ∈ s, x ∈ openSegment ℝ 0 y
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>h₀ : 0 ∈ s<VAR>absorbs : Absorbent ℝ s<GOAL>{x | gauge s x < 1} ⊆ s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ s<GOAL>gauge s x ≤ 1
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>absorbs : Absorbent ℝ s<VAR>x y : E<GOAL>gauge s (x + y) ≤ gauge s x + gauge s y
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<GOAL>s ⊆ {x | gauge s x ≤ 1}
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>h₀ : 0 ∈ s<VAR>absorbs : Absorbent ℝ s<VAR>a : ℝ<GOAL>Convex ℝ {x | gauge s x ≤ a}
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>hs : Balanced ℝ s<GOAL>StarConvex ℝ 0 s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>a : ℝ<VAR>hs₀ : StarConvex ℝ 0 s<VAR>hs₂ : Absorbs ℝ s {x}<VAR>hx : x ∉ a • s<GOAL>a ≤ gauge s x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs₁ : StarConvex ℝ 0 s<VAR>hs₂ : Absorbs ℝ s {x}<VAR>hx : x ∉ s<GOAL>1 ≤ gauge s x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>α : Type u_4<VAR>LinearOrderedField α<VAR>MulActionWithZero α ℝ<VAR>OrderedSMul α ℝ<VAR>MulActionWithZero α E<VAR>IsScalarTower α ℝ (Set E)<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>x : E<GOAL>gauge s (a • x) = a • gauge s x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>α : Type u_4<VAR>LinearOrderedField α<VAR>MulActionWithZero α ℝ<VAR>OrderedSMul α ℝ<VAR>MulActionWithZero α E<VAR>SMulCommClass α ℝ ℝ<VAR>IsScalarTower α ℝ ℝ<VAR>IsScalarTower α ℝ E<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>gauge (a • s) = a⁻¹ • gauge s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>α : Type u_4<VAR>LinearOrderedField α<VAR>MulActionWithZero α ℝ<VAR>OrderedSMul α ℝ<VAR>Module α E<VAR>SMulCommClass α ℝ ℝ<VAR>IsScalarTower α ℝ ℝ<VAR>IsScalarTower α ℝ E<VAR>s : Set E<VAR>symmetric : ∀ x ∈ s, -x ∈ s<VAR>a : α<GOAL>gauge (a • s) = |a|⁻¹ • gauge s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>IsScalarTower ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<VAR>r : 𝕜<VAR>x : E<GOAL>gauge s (‖r‖ • x) = gauge s (r • x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>IsScalarTower ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<VAR>r : 𝕜<VAR>x : E<GOAL>gauge s (r • x) = ‖r‖ * gauge s x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>ha : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<GOAL>Filter.comap (gauge s) (𝓝 0) ≤ 𝓝 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>hs : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<GOAL>gauge s x = 0 ↔ x = 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>hs : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<GOAL>0 < gauge s x ↔ x ≠ 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<GOAL>interior s ⊆ {x | gauge s x < 1}
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : IsOpen s<GOAL>{x | gauge s x < 1} = s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hs₂ : IsOpen s<VAR>x : E<VAR>hx : x ∈ s<GOAL>gauge s x < 1
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>x : E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hs₂ : IsOpen s<VAR>hx : x ∈ ε • s<GOAL>gauge s x < ε
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>ha : Absorbent ℝ s<VAR>h : gauge s x ≤ 1<GOAL>x ∈ closure s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>ha : Absorbent ℝ s<VAR>h : gauge s x = 1<GOAL>x ∈ frontier s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hs : s ∈ 𝓝 0<GOAL>Filter.Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hs : s ∈ 𝓝 0<GOAL>Filter.Tendsto (gauge s) (𝓝 0) (𝓝 0)
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hs : s ∈ 𝓝 0<GOAL>ContinuousAt (gauge s) 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>h₀ : s ∈ 𝓝 0<GOAL>Filter.comap (gauge s) (𝓝 0) = 𝓝 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>ContinuousAt (gauge s) x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>Continuous (gauge s)
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>{x | gauge s x < 1} = interior s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>gauge s x < 1 ↔ x ∈ interior s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>gauge s x ≤ 1 ↔ x ∈ closure s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>gauge s x = 1 ↔ x ∈ frontier s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>IsScalarTower ℝ 𝕜 E<VAR>hs₀ : Balanced 𝕜 s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : Absorbent ℝ s<VAR>x : E<GOAL>(gaugeSeminorm hs₀ hs₁ hs₂) x = gauge s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>IsScalarTower ℝ 𝕜 E<VAR>hs₀ : Balanced 𝕜 s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : Absorbent ℝ s<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hs : IsOpen s<VAR>x : E<VAR>hx : x ∈ s<GOAL>(gaugeSeminorm hs₀ hs₁ hs₂) x < 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>IsScalarTower ℝ 𝕜 E<VAR>hs₀ : Balanced 𝕜 s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : Absorbent ℝ s<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>hs : IsOpen s<GOAL>(gaugeSeminorm hs₀ hs₁ hs₂).ball 0 1 = s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>p : Seminorm ℝ E<GOAL>gauge (p.ball 0 1) = ⇑p
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>p : Seminorm ℝ E<GOAL>gaugeSeminorm ⋯ ⋯ ⋯ = p
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<GOAL>gauge (Metric.ball 0 1) x = ‖x‖
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x : E<GOAL>gauge (Metric.ball 0 r) x = ‖x‖ / r
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : E<GOAL>gauge (Metric.ball 0 r) x = ‖x‖ / r
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>gauge (closure 0) = 0
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x : E<GOAL>gauge (Metric.closedBall 0 r) x = ‖x‖ / r
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x : E<VAR>hs : Metric.ball 0 r ⊆ s<GOAL>r * gauge s x ≤ ‖x‖
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ≥0<VAR>hc : Convex ℝ s<VAR>hr : 0 < r<VAR>hs : Metric.ball 0 ↑r ⊆ s<GOAL>LipschitzWith r⁻¹ (gauge s)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>hc : Convex ℝ s<VAR>h₀ : s ∈ 𝓝 0<GOAL>∃ K, LipschitzWith K (gauge s)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>hc : Convex ℝ s<VAR>h₀ : s ∈ 𝓝 0<GOAL>UniformContinuous (gauge s)
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x : E<VAR>hs : Absorbent ℝ s<VAR>hr : 0 ≤ r<VAR>hsr : s ⊆ Metric.closedBall 0 r<GOAL>‖x‖ / r ≤ gauge s x
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>TopologicalSpace X<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>g : ι → X → E<VAR>t : Set E<VAR>x : X<VAR>hx : x ∈ s<VAR>hg : ∀ (i : ι), (f i) x ≠ 0 → g i x ∈ t<VAR>ht : Convex ℝ t<GOAL>∑ᶠ (i : ι), (f i) x • g i x ∈ t
<VAR>X : Type u_2<VAR>E : Type u_3<VAR>TopologicalSpace X<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>NormalSpace X<VAR>ParacompactSpace X<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>t : X → Set E<VAR>ht : ∀ (x : X), Convex ℝ (t x)<VAR>H : ∀ (x : X), ∃ U ∈ 𝓝 x, ∃ g, ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y<GOAL>∃ g, ∀ (x : X), g x ∈ t x
<VAR>X : Type u_2<VAR>E : Type u_3<VAR>TopologicalSpace X<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>NormalSpace X<VAR>ParacompactSpace X<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>t : X → Set E<VAR>ht : ∀ (x : X), Convex ℝ (t x)<VAR>H : ∀ (x : X), ∃ c, ∀ᶠ (y : X) in 𝓝 x, c ∈ t y<GOAL>∃ g, ∀ (x : X), g x ∈ t x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>StrictConvexSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<VAR>p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>dist p₂ p < max (dist p₁ p) (dist p₃ p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>StrictConvexSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<VAR>p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<GOAL>dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>StrictConvexSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p ≤ r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>Wbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>StrictConvexSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>r : ℝ<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : dist p₁ p = r<VAR>hp₂ : dist p₂ p < r<VAR>hp₃ : dist p₃ p = r<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>Sbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>StrictConvexSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b c : P<GOAL>dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
<VAR>E : Type u_3<VAR>PE : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>r : ℝ<VAR>x y z : PE<VAR>hxy : dist x y = r * dist x z<VAR>hyz : dist y z = (1 - r) * dist x z<GOAL>y = (AffineMap.lineMap x z) r
<VAR>E : Type u_3<VAR>PE : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>x y z : PE<VAR>hx : dist x y = dist x z / 2<VAR>hy : dist y z = dist x z / 2<GOAL>y = midpoint ℝ x z
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>StrictConvexSpace ℝ E<VAR>MetricSpace PE<VAR>MetricSpace PF<VAR>NormedAddTorsor E PE<VAR>NormedAddTorsor F PF<VAR>f : PF → PE<VAR>hi : Isometry f<GOAL>⇑hi.affineIsometryOfStrictConvexSpace = f
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>StrictConvexSpace ℝ E<VAR>MetricSpace PE<VAR>MetricSpace PF<VAR>NormedAddTorsor E PE<VAR>NormedAddTorsor F PF<VAR>f : PF → PE<VAR>hi : Isometry f<VAR>p : PF<GOAL>hi.affineIsometryOfStrictConvexSpace p = f p
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>SMul 𝕜 E<VAR>ContinuousConstSMul 𝕜 E<VAR>K : ConvexCone 𝕜 E<GOAL>↑K.closure = closure ↑K
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>SMul 𝕜 E<VAR>ContinuousConstSMul 𝕜 E<VAR>K : ConvexCone 𝕜 E<VAR>a : E<GOAL>a ∈ K.closure ↔ a ∈ closure ↑K
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>SMul 𝕜 E<VAR>ContinuousConstSMul 𝕜 E<VAR>K L : ConvexCone 𝕜 E<GOAL>K.closure = L ↔ closure ↑K = ↑L
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>Module 𝕜 E<VAR>ContinuousConstSMul 𝕜 E<VAR>K : PointedCone 𝕜 E<GOAL>(↑K).closure.Pointed
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>Module 𝕜 E<VAR>ContinuousConstSMul 𝕜 E<VAR>K : PointedCone 𝕜 E<GOAL>↑K.closure = closure ↑K
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>Module 𝕜 E<VAR>ContinuousConstSMul 𝕜 E<VAR>K : PointedCone 𝕜 E<VAR>a : E<GOAL>a ∈ K.closure ↔ a ∈ closure ↑K
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>Module 𝕜 E<VAR>ContinuousConstSMul 𝕜 E<VAR>K L : PointedCone 𝕜 E<GOAL>K.closure = L ↔ closure ↑K = ↑L
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : outParam (A → Prop)<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>self : ContinuousFunctionalCalculus R p<VAR>a : A<GOAL>p a → ∃ φ, ClosedEmbedding ⇑φ ∧ φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a ∧ (∀ (f : C(↑(spectrum R a), R)), spectrum R (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(spectrum R a), R)), p (φ f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : outParam (A → Prop)<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>self : ContinuousFunctionalCalculus R p<GOAL>p 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>self : UniqueContinuousFunctionalCalculus R A<VAR>s : Set R<VAR>CompactSpace ↑s<VAR>φ ψ : C(↑s, R) →⋆ₐ[R] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ (ContinuousMap.restrict s (ContinuousMap.id R)) = ψ (ContinuousMap.restrict s (ContinuousMap.id R))<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>self : UniqueContinuousFunctionalCalculus R A<VAR>a : A<GOAL>CompactSpace ↑(spectrum R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>UniqueContinuousFunctionalCalculus R A<VAR>a : A<VAR>φ ψ : C(↑(spectrum R a), R) →⋆ₐ[R] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = ψ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<GOAL>ClosedEmbedding ⇑(cfcHom ha)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<GOAL>(cfcHom ha) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), R)<GOAL>spectrum R ((cfcHom ha) f) = Set.range ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), R)<GOAL>p ((cfcHom ha) f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>UniqueContinuousFunctionalCalculus R A<VAR>φ : C(↑(spectrum R a), R) →⋆ₐ[R] A<VAR>hφ₁ : Continuous ⇑φ<VAR>hφ₂ : φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a<GOAL>cfcHom ha = φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>UniqueContinuousFunctionalCalculus R A<VAR>f : C(↑(spectrum R a), R)<VAR>f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))<VAR>hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)<VAR>g : C(↑(spectrum R ((cfcHom ha) f)), R)<GOAL>(cfcHom ha) (g.comp f') = (cfcHom ⋯) g
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<GOAL>cfc f a = if h : p a ∧ ContinuousOn f (spectrum R a) then (cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } else 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>ha : p a := by cfc_tac<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<GOAL>cfc f a = (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>ι : Type u_3<VAR>f : ι → R → R<VAR>a : A<VAR>ha : p a := by cfc_tac<VAR>hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a) := by cfc_cont_tac<GOAL>(fun i => cfc (f i) a) = fun i => (cfcHom ha) { toFun := (spectrum R a).restrict (f i), continuous_toFun := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>ha : ¬(p a ∧ ContinuousOn f (spectrum R a))<GOAL>cfc f a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>ha : ¬p a<GOAL>cfc f a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf : ¬ContinuousOn f (spectrum R a)<GOAL>cfc f a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(spectrum R a), R)<GOAL>(cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>P : A → Prop<VAR>a : A<VAR>f : R → R<VAR>h₀ : P 0<VAR>haf : ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a), P ((cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })<GOAL>P (cfc f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc id a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => x) a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>ha : p a := by cfc_tac<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<GOAL>spectrum R (cfc f a) = f '' spectrum R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => r) a = (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<GOAL>p 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<GOAL>p (cfc f a)