ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>k : ℕ<VAR>h : ↑‖x‖₊ < p.radius<GOAL>‖p.changeOrigin x k‖₊ ≤ ∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<GOAL>p.radius - ↑‖x‖₊ ≤ (p.changeOrigin x).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>k : ℕ<VAR>hr : 0 < p.radius<GOAL>HasFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius<GOAL>(p.changeOrigin x).sum y = p.sum (x + y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>rp : p.radius > 0<VAR>n : ℕ<GOAL>AnalyticAt 𝕜 (fun x => p.changeOrigin x n) 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑‖y‖₊ < r<GOAL>HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ↑‖y‖₊)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : y ∈ EMetric.ball x r<GOAL>AnalyticAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>AnalyticOn 𝕜 f (EMetric.ball x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<GOAL>IsOpen {x | AnalyticAt 𝕜 f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>x : E<VAR>h : AnalyticAt 𝕜 f x<GOAL>∀ᶠ (y : E) in 𝓝 x, AnalyticAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>x : E<VAR>h : AnalyticAt 𝕜 f x<GOAL>∃ s ∈ 𝓝 x, AnalyticOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>x : E<VAR>h : AnalyticAt 𝕜 f x<GOAL>∃ r, 0 < r ∧ AnalyticOn 𝕜 f (Metric.ball x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<GOAL>HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<GOAL>HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • p.coeff n) (f z)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>self : Geometry.SimplicialComplex 𝕜 E<GOAL>∅ ∉ self.faces
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>self : Geometry.SimplicialComplex 𝕜 E<VAR>s : Finset E<GOAL>s ∈ self.faces → AffineIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>self : Geometry.SimplicialComplex 𝕜 E<VAR>s t : Finset E<GOAL>s ∈ self.faces → t ∈ self.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>self : Geometry.SimplicialComplex 𝕜 E<VAR>s t : Finset E<GOAL>s ∈ self.faces → t ⊆ s → t ≠ ∅ → t ∈ self.faces
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>x : E<GOAL>x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ (convexHull 𝕜) ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>s : Finset E<VAR>hs : s ∈ K.faces<GOAL>(convexHull 𝕜) ↑s ⊆ K.space
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>s : Finset E<VAR>hs : s ∈ K.faces<GOAL>↑s ⊆ K.space
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>hs : s ∈ K.faces<VAR>ht : t ∈ K.faces<GOAL>(convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) (↑s ∩ ↑t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>hs : s ∈ K.faces<VAR>ht : t ∈ K.faces<GOAL>Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∨ ∃ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>faces : Set (Finset E)<VAR>indep : ∀ s ∈ faces, AffineIndependent 𝕜 Subtype.val<VAR>down_closed : ∀ s ∈ faces, ∀ t ⊆ s, t ∈ faces<VAR>inter_subset_convexHull : ∀ s ∈ faces, ∀ t ∈ faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)<GOAL>(Geometry.SimplicialComplex.ofErase faces indep down_closed inter_subset_convexHull).faces = faces \ {∅}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>faces : Set (Finset E)<VAR>subset : faces ⊆ K.faces<VAR>down_closed : ∀ {s t : Finset E}, s ∈ faces → t ⊆ s → t ∈ faces<GOAL>(K.ofSubcomplex faces subset down_closed).faces = faces
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>x : E<GOAL>x ∈ K.vertices ↔ {x} ∈ K.faces
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<GOAL>K.vertices = ⋃ k ∈ K.faces, ↑k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<GOAL>K.vertices ⊆ K.space
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>s : Finset E<VAR>x : E<VAR>hx : x ∈ K.vertices<VAR>hs : s ∈ K.faces<GOAL>x ∈ (convexHull 𝕜) ↑s ↔ x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>hs : s ∈ K.faces<VAR>ht : t ∈ K.faces<GOAL>(convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t ↔ s ⊆ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>s : Finset E<GOAL>s ∈ K.facets ↔ s ∈ K.faces ∧ ∀ t ∈ K.faces, s ⊆ t → s = t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<GOAL>K.facets ⊆ K.faces
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>K : Geometry.SimplicialComplex 𝕜 E<VAR>s : Finset E<VAR>hs : s ∈ K.faces<GOAL>s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>⊥.faces = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>⊥.space = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>⊥.facets = ∅
<VAR>s : Set ℝ<GOAL>Convex ℝ s ↔ IsPreconnected s
<VAR>ι : Type u_1<VAR>Fintype ι<GOAL>stdSimplex ℝ ι ⊆ Metric.closedBall 0 1
<VAR>ι : Type u_1<VAR>Fintype ι<GOAL>Bornology.IsBounded (stdSimplex ℝ ι)
<VAR>ι : Type u_1<VAR>Fintype ι<GOAL>IsClosed (stdSimplex ℝ ι)
<VAR>ι : Type u_1<VAR>Fintype ι<GOAL>IsCompact (stdSimplex ℝ ι)
<VAR>x : ↑(Set.Icc 0 1)<GOAL>↑(stdSimplexHomeomorphUnitInterval.symm x) = ![↑x, 1 - ↑x]
<VAR>f : ↑(stdSimplex ℝ (Fin 2))<GOAL>↑(stdSimplexHomeomorphUnitInterval f) = ↑f 0
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedRing 𝕜<VAR>DenselyOrdered 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>x y : E<GOAL>[x-[𝕜]y] ⊆ closure (openSegment 𝕜 x y)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedRing 𝕜<VAR>DenselyOrdered 𝕜<VAR>PseudoMetricSpace 𝕜<VAR>OrderTopology 𝕜<VAR>ProperSpace 𝕜<VAR>CompactIccSpace 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>ContinuousAdd E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>x y : E<GOAL>closure (openSegment 𝕜 x y) = [x-[𝕜]y]
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • interior s + b • closure s ⊆ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • interior s + b • s ⊆ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • closure s + b • interior s ⊆ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • s + b • interior s ⊆ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ interior s<VAR>hy : y ∈ closure s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ interior s<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ closure s<VAR>hy : y ∈ interior s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ interior s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ interior s<VAR>hy : y ∈ closure s<GOAL>openSegment 𝕜 x y ⊆ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ interior s<VAR>hy : y ∈ s<GOAL>openSegment 𝕜 x y ⊆ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ closure s<VAR>hy : y ∈ interior s<GOAL>openSegment 𝕜 x y ⊆ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ interior s<GOAL>openSegment 𝕜 x y ⊆ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ closure s<VAR>hy : y ∈ interior s<VAR>t : 𝕜<VAR>ht : t ∈ Set.Ioc 0 1<GOAL>x + t • (y - x) ∈ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ interior s<VAR>t : 𝕜<VAR>ht : t ∈ Set.Ioc 0 1<GOAL>x + t • (y - x) ∈ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ closure s<VAR>hy : x + y ∈ interior s<VAR>t : 𝕜<VAR>ht : t ∈ Set.Ioc 0 1<GOAL>x + t • y ∈ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : x + y ∈ interior s<VAR>t : 𝕜<VAR>ht : t ∈ Set.Ioc 0 1<GOAL>x + t • y ∈ interior s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>Convex 𝕜 (interior s)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>Convex 𝕜 (closure s)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ∃ c, (AffineMap.lineMap x y) c ∈ interior s<GOAL>StrictConvex 𝕜 s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty<GOAL>StrictConvex 𝕜 s
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : s.Finite<GOAL>IsCompact ((convexHull ℝ) s)
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>T2Space E<VAR>s : Set E<VAR>hs : s.Finite<GOAL>IsClosed ((convexHull ℝ) s)
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<VAR>t : ℝ<VAR>ht : 1 < t<GOAL>closure s ⊆ ⇑(AffineMap.homothety x t) '' interior s
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<VAR>t : ℝ<VAR>ht : 1 < t<GOAL>closure s ⊆ interior (⇑(AffineMap.homothety x t) '' s)
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<VAR>t : ℝ<VAR>ht : 1 < t<GOAL>s ⊆ interior (⇑(AffineMap.homothety x t) '' s)
<VAR>E : Type u_4<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>x y : E<VAR>s : Set E<VAR>h : [x-[ℝ]y] ⊆ s<GOAL>JoinedIn s x y
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>hconv : Convex ℝ s<VAR>hne : s.Nonempty<GOAL>IsPathConnected s
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>h : Convex ℝ s<VAR>hne : s.Nonempty<GOAL>IsConnected s
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>h : Convex ℝ s<GOAL>IsPreconnected s
<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<GOAL>PathConnectedSpace E
<VAR>E : Type u_4<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>p q : Submodule ℝ E<VAR>hpq : IsCompl p q<VAR>hpc : IsPathConnected {0}ᶜ<GOAL>IsPathConnected (↑q)ᶜ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>Function.Injective PointedCone.toConvexCone
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : PointedCone 𝕜 E<GOAL>(↑S).Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S T : PointedCone 𝕜 E<VAR>h : ∀ (x : E), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : ConvexCone 𝕜 E<VAR>hS : S.Pointed<VAR>x : E<GOAL>x ∈ ConvexCone.toPointedCone hS ↔ x ∈ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : ConvexCone 𝕜 E<VAR>hS : S.Pointed<GOAL>↑(ConvexCone.toPointedCone hS) = S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>S : PointedCone 𝕜 E<VAR>f : E →ₗ[𝕜] F<GOAL>↑(PointedCone.map f S) = ConvexCone.map f ↑S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>S : PointedCone 𝕜 E<VAR>f : E →ₗ[𝕜] F<GOAL>↑(PointedCone.map f S) = ⇑f '' ↑S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>S : PointedCone 𝕜 E<VAR>y : F<GOAL>y ∈ PointedCone.map f S ↔ ∃ x ∈ S, f x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>AddCommMonoid G<VAR>Module 𝕜 G<VAR>g : F →ₗ[𝕜] G<VAR>f : E →ₗ[𝕜] F<VAR>S : PointedCone 𝕜 E<GOAL>PointedCone.map g (PointedCone.map f S) = PointedCone.map (g ∘ₗ f) S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : PointedCone 𝕜 E<GOAL>PointedCone.map LinearMap.id S = S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>S : PointedCone 𝕜 F<GOAL>↑(PointedCone.comap f S) = ⇑f ⁻¹' ↑S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : PointedCone 𝕜 E<GOAL>PointedCone.comap LinearMap.id S = S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>AddCommMonoid G<VAR>Module 𝕜 G<VAR>g : F →ₗ[𝕜] G<VAR>f : E →ₗ[𝕜] F<VAR>S : PointedCone 𝕜 G<GOAL>PointedCone.comap f (PointedCone.comap g S) = PointedCone.comap (g ∘ₗ f) S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>S : PointedCone 𝕜 F<VAR>x : E<GOAL>x ∈ PointedCone.comap f S ↔ f x ∈ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>x : E<GOAL>x ∈ PointedCone.positive 𝕜 E ↔ 0 ≤ x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<GOAL>↑(PointedCone.positive 𝕜 E) = ConvexCone.positive 𝕜 E
<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>S : PointedCone ℝ E<GOAL>↑S.dual = (↑S).innerDualCone
<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>S : PointedCone ℝ E<VAR>y : E<GOAL>y ∈ S.dual ↔ ∀ ⦃x : E⦄, x ∈ S → 0 ≤ ⟪x, y⟫_ℝ
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>y : H<VAR>s : Set H<GOAL>y ∈ s.innerDualCone ↔ ∀ x ∈ s, 0 ≤ ⟪x, y⟫_ℝ
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<GOAL>∅.innerDualCone = ⊤
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<GOAL>Set.innerDualCone 0 = ⊤
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<GOAL>Set.univ.innerDualCone = 0
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>s t : Set H<VAR>h : t ⊆ s<GOAL>s.innerDualCone ≤ t.innerDualCone
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>s : Set H<GOAL>s.innerDualCone.Pointed
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>x : H<GOAL>{x}.innerDualCone = ConvexCone.comap ((innerₛₗ ℝ) x) (ConvexCone.positive ℝ ℝ)
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>s t : Set H<GOAL>(s ∪ t).innerDualCone = s.innerDualCone ⊓ t.innerDualCone
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>x : H<VAR>s : Set H<GOAL>(insert x s).innerDualCone = {x}.innerDualCone ⊓ s.innerDualCone
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>ι : Sort u_6<VAR>f : ι → Set H<GOAL>(⋃ i, f i).innerDualCone = ⨅ i, (f i).innerDualCone
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>S : Set (Set H)<GOAL>(⋃₀ S).innerDualCone = sInf (Set.innerDualCone '' S)
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>s : Set H<GOAL>↑s.innerDualCone = ⋂ i, ↑{↑i}.innerDualCone
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>s : Set H<GOAL>IsClosed ↑s.innerDualCone
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>K : ConvexCone ℝ H<VAR>ne : (↑K).Nonempty<VAR>hc : IsClosed ↑K<GOAL>K.Pointed
<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace ℝ H<VAR>CompleteSpace H<VAR>K : ConvexCone ℝ H<VAR>ne : (↑K).Nonempty<VAR>hc : IsClosed ↑K<VAR>b : H<VAR>disj : b ∉ K<GOAL>∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0