ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<GOAL>(↑(↑K).innerDualCone).innerDualCone = K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>self : ProperCone 𝕜 E<GOAL>IsClosed self.carrier
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<GOAL>Function.Injective ProperCone.toPointedCone
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>S T : ProperCone 𝕜 E<VAR>h : ∀ (x : E), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>x : E<VAR>K : ProperCone 𝕜 E<GOAL>x ∈ ↑K ↔ x ∈ K
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>K : ProperCone 𝕜 E<GOAL>(↑K).Nonempty
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>K : ProperCone 𝕜 E<GOAL>IsClosed ↑K
<VAR>𝕜 : Type u_2<VAR>E : Type u_1<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>TopologicalSpace E<VAR>OrderClosedTopology E<VAR>x : E<GOAL>x ∈ ProperCone.positive 𝕜 E ↔ 0 ≤ x
<VAR>𝕜 : Type u_2<VAR>E : Type u_1<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>TopologicalSpace E<VAR>OrderClosedTopology E<GOAL>↑↑(ProperCone.positive 𝕜 E) = ConvexCone.positive 𝕜 E
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>Module 𝕜 E<VAR>x : E<GOAL>x ∈ 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>Module 𝕜 E<GOAL>↑↑0 = 0
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>Module 𝕜 E<GOAL>(↑↑0).Pointed
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>K : ProperCone ℝ E<GOAL>(↑↑K).Pointed
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>K : ProperCone ℝ E<GOAL>↑(ProperCone.map f K) = (PointedCone.map ↑f ↑K).closure
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>K : ProperCone ℝ E<VAR>y : F<GOAL>y ∈ ProperCone.map f K ↔ y ∈ (PointedCone.map ↑f ↑K).closure
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>K : ProperCone ℝ E<GOAL>ProperCone.map (ContinuousLinearMap.id ℝ E) K = K
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>K : ProperCone ℝ E<GOAL>↑↑K.dual = (↑K).innerDualCone
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>K : ProperCone ℝ E<VAR>y : E<GOAL>y ∈ K.dual ↔ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪x, y⟫_ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>S : ProperCone ℝ F<GOAL>↑(ProperCone.comap f S) = ⇑f ⁻¹' ↑S
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>S : ConvexCone ℝ E<GOAL>ConvexCone.comap LinearMap.id S = S
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>InnerProductSpace ℝ G<VAR>g : F →L[ℝ] G<VAR>f : E →L[ℝ] F<VAR>S : ProperCone ℝ G<GOAL>ProperCone.comap f (ProperCone.comap g S) = ProperCone.comap (g.comp f) S
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>S : ProperCone ℝ F<VAR>x : E<GOAL>x ∈ ProperCone.comap f S ↔ f x ∈ S
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>CompleteSpace E<VAR>K : ProperCone ℝ E<GOAL>K.dual.dual = K
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>CompleteSpace E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<GOAL>b ∈ ProperCone.map f K ↔ ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>CompleteSpace E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>CompleteSpace F<VAR>K : ProperCone ℝ E<VAR>f : E →L[ℝ] F<VAR>b : F<VAR>disj : b ∉ ProperCone.map f K<GOAL>∃ y, (ContinuousLinearMap.adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>self : ConvexCone 𝕜 E<VAR>x : E<GOAL>x ∈ self.carrier → ∀ ⦃y : E⦄, y ∈ self.carrier → x + y ∈ self.carrier
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>self : ConvexCone 𝕜 E<VAR>c : 𝕜<GOAL>0 < c → ∀ ⦃x : E⦄, x ∈ self.carrier → c • x ∈ self.carrier
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>h₁ : ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : E⦄, x ∈ s → c • x ∈ s<VAR>h₂ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x + y ∈ s<GOAL>↑{ carrier := s, smul_mem' := h₁, add_mem' := h₂ } = s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>h₁ : ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : E⦄, x ∈ s → c • x ∈ s<VAR>h₂ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x + y ∈ s<VAR>x : E<GOAL>x ∈ { carrier := s, smul_mem' := h₁, add_mem' := h₂ } ↔ x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S T : ConvexCone 𝕜 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>SMul 𝕜 E<VAR>S : ConvexCone 𝕜 E<VAR>c : 𝕜<VAR>x : E<VAR>hc : 0 < c<VAR>hx : x ∈ S<GOAL>c • x ∈ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S : ConvexCone 𝕜 E<VAR>x : E<VAR>hx : x ∈ S<VAR>y : E<VAR>hy : y ∈ S<GOAL>x + y ∈ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S T : ConvexCone 𝕜 E<GOAL>↑(S ⊓ T) = ↑S ∩ ↑T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S T : ConvexCone 𝕜 E<VAR>x : E<GOAL>x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S : Set (ConvexCone 𝕜 E)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>S : Set (ConvexCone 𝕜 E)<GOAL>x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>ι : Sort u_5<VAR>f : ι → ConvexCone 𝕜 E<GOAL>↑(iInf f) = ⋂ i, ↑(f i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>ι : Sort u_5<VAR>x : E<VAR>f : ι → ConvexCone 𝕜 E<GOAL>x ∈ iInf f ↔ ∀ (i : ι), x ∈ f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<GOAL>(x ∈ ⊥) = False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<GOAL>↑⊥ = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<GOAL>x ∈ ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<GOAL>↑⊤ = Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : ConvexCone 𝕜 E<GOAL>Convex 𝕜 ↑S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>S : ConvexCone 𝕜 E<VAR>f : E →ₗ[𝕜] F<GOAL>↑(ConvexCone.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>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>S : ConvexCone 𝕜 E<VAR>y : F<GOAL>y ∈ ConvexCone.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>AddCommMonoid F<VAR>AddCommMonoid G<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module 𝕜 G<VAR>g : F →ₗ[𝕜] G<VAR>f : E →ₗ[𝕜] F<VAR>S : ConvexCone 𝕜 E<GOAL>ConvexCone.map g (ConvexCone.map f S) = ConvexCone.map (g ∘ₗ f) S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : ConvexCone 𝕜 E<GOAL>ConvexCone.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>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>S : ConvexCone 𝕜 F<GOAL>↑(ConvexCone.comap f S) = ⇑f ⁻¹' ↑S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : ConvexCone 𝕜 E<GOAL>ConvexCone.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>AddCommMonoid F<VAR>AddCommMonoid G<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module 𝕜 G<VAR>g : F →ₗ[𝕜] G<VAR>f : E →ₗ[𝕜] F<VAR>S : ConvexCone 𝕜 G<GOAL>ConvexCone.comap f (ConvexCone.comap g S) = ConvexCone.comap (g ∘ₗ f) S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>S : ConvexCone 𝕜 F<VAR>x : E<GOAL>x ∈ ConvexCone.comap f S ↔ f x ∈ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommMonoid E<VAR>MulAction 𝕜 E<VAR>S : ConvexCone 𝕜 E<VAR>c : 𝕜<VAR>hc : 0 < c<VAR>x : E<GOAL>c • x ∈ S ↔ x ∈ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>S : ConvexCone 𝕜 E<VAR>h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S<GOAL>OrderedSMul 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S : ConvexCone 𝕜 E<GOAL>S.Pointed ↔ ¬S.Blunt
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S : ConvexCone 𝕜 E<GOAL>S.Blunt ↔ ¬S.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S T : ConvexCone 𝕜 E<VAR>h : S ≤ T<GOAL>S.Pointed → T.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S T : ConvexCone 𝕜 E<VAR>h : T ≤ S<GOAL>S.Blunt → T.Blunt
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>S : ConvexCone 𝕜 E<GOAL>S.Salient ↔ ¬S.Flat
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>S T : ConvexCone 𝕜 E<VAR>h : S ≤ T<GOAL>S.Flat → T.Flat
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>S T : ConvexCone 𝕜 E<VAR>h : T ≤ S<GOAL>S.Salient → T.Salient
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>S : ConvexCone 𝕜 E<VAR>hS : S.Flat<GOAL>S.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>S : ConvexCone 𝕜 E<GOAL>S.Blunt → S.Salient
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<GOAL>x ∈ 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>↑0 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>ConvexCone.Pointed 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>K₁ K₂ : ConvexCone 𝕜 E<VAR>a : E<GOAL>a ∈ K₁ + K₂ ↔ ∃ x ∈ K₁, ∃ y ∈ K₂, x + y = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : Submodule 𝕜 E<GOAL>↑S.toConvexCone = ↑S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>S : Submodule 𝕜 E<GOAL>x ∈ S.toConvexCone ↔ x ∈ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S T : Submodule 𝕜 E<GOAL>S.toConvexCone ≤ T.toConvexCone ↔ S ≤ T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>⊥.toConvexCone = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>⊤.toConvexCone = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S T : Submodule 𝕜 E<GOAL>(S ⊓ T).toConvexCone = S.toConvexCone ⊓ T.toConvexCone
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>S : Submodule 𝕜 E<GOAL>S.toConvexCone.Pointed
<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 ∈ ConvexCone.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>↑(ConvexCone.positive 𝕜 E) = Set.Ici 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<GOAL>(ConvexCone.positive 𝕜 E).Salient
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<GOAL>(ConvexCone.positive 𝕜 E).Pointed
<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 ∈ ConvexCone.strictlyPositive 𝕜 E ↔ 0 < x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<GOAL>↑(ConvexCone.strictlyPositive 𝕜 E) = Set.Ioi 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<GOAL>ConvexCone.strictlyPositive 𝕜 E ≤ ConvexCone.positive 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<GOAL>(ConvexCone.strictlyPositive 𝕜 E).Salient
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<GOAL>(ConvexCone.strictlyPositive 𝕜 E).Blunt
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<GOAL>x ∈ Convex.toCone s hs ↔ ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<GOAL>x ∈ Convex.toCone s hs ↔ ∃ c, 0 < c ∧ c • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>s ⊆ ↑(Convex.toCone s hs)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>IsLeast {t | s ⊆ ↑t} (Convex.toCone s hs)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>Convex.toCone s hs = sInf {t | s ⊆ ↑t}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>IsLeast {t | s ⊆ ↑t} (Convex.toCone ((convexHull 𝕜) s) ⋯)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Convex.toCone ((convexHull 𝕜) s) ⋯ = sInf {t | s ⊆ ↑t}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A : Set E<GOAL>IsExtreme 𝕜 A A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A B C : Set E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hBC : IsExtreme 𝕜 B C<GOAL>IsExtreme 𝕜 A C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<GOAL>AntiSymmetric (IsExtreme 𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A B C : Set E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hAC : IsExtreme 𝕜 A C<GOAL>IsExtreme 𝕜 A (B ∩ C)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A B C : Set E<VAR>hAC : IsExtreme 𝕜 A C<VAR>hBA : B ⊆ A<VAR>hCB : C ⊆ B<GOAL>IsExtreme 𝕜 B C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A : Set E<VAR>ι : Sort u_6<VAR>Nonempty ι<VAR>F : ι → Set E<VAR>hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)<GOAL>IsExtreme 𝕜 A (⋂ i, F i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A : Set E<VAR>F : Set (Set E)<VAR>hF : F.Nonempty<VAR>hA : ∀ B ∈ F, IsExtreme 𝕜 A B<GOAL>IsExtreme 𝕜 A (⋂ B ∈ F, B)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A : Set E<VAR>F : Set (Set E)<VAR>hF : F.Nonempty<VAR>hAF : ∀ B ∈ F, IsExtreme 𝕜 A B<GOAL>IsExtreme 𝕜 A (⋂₀ F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A : Set E<VAR>x : E<GOAL>x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A : Set E<VAR>x : E<GOAL>IsExtreme 𝕜 A {x} ↔ x ∈ Set.extremePoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A : Set E<GOAL>Set.extremePoints 𝕜 A ⊆ A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<GOAL>Set.extremePoints 𝕜 ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<GOAL>Set.extremePoints 𝕜 {x} = {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A B : Set E<VAR>hBA : B ⊆ A<GOAL>B ∩ Set.extremePoints 𝕜 A ⊆ Set.extremePoints 𝕜 B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A B : Set E<VAR>hAB : IsExtreme 𝕜 A B<GOAL>Set.extremePoints 𝕜 B ⊆ Set.extremePoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>A B : Set E<VAR>hAB : IsExtreme 𝕜 A B<GOAL>Set.extremePoints 𝕜 B = B ∩ Set.extremePoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>A B : Set E<VAR>hA : Convex 𝕜 A<VAR>hAB : IsExtreme 𝕜 A B<GOAL>Convex 𝕜 (A \ B)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set E<VAR>t : Set F<GOAL>Set.extremePoints 𝕜 (s ×ˢ t) = Set.extremePoints 𝕜 s ×ˢ Set.extremePoints 𝕜 t
<VAR>𝕜 : Type u_1<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>OrderedSemiring 𝕜<VAR>(i : ι) → AddCommGroup (π i)<VAR>(i : ι) → Module 𝕜 (π i)<VAR>s : (i : ι) → Set (π i)<GOAL>Set.extremePoints 𝕜 (Set.univ.pi s) = Set.univ.pi fun i => Set.extremePoints 𝕜 (s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>L : Type u_6<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>EquivLike L E F<VAR>LinearEquivClass L 𝕜 E F<VAR>f : L<VAR>s : Set E<GOAL>⇑f '' Set.extremePoints 𝕜 s = Set.extremePoints 𝕜 (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>DenselyOrdered 𝕜<VAR>NoZeroSMulDivisors 𝕜 E<VAR>A : Set E<VAR>x : E<GOAL>x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>DenselyOrdered 𝕜<VAR>NoZeroSMulDivisors 𝕜 E<VAR>A : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<GOAL>x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ Convex 𝕜 (A \ {x})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>DenselyOrdered 𝕜<VAR>NoZeroSMulDivisors 𝕜 E<VAR>A : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<GOAL>x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜) (A \ {x})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>DenselyOrdered 𝕜<VAR>NoZeroSMulDivisors 𝕜 E<VAR>A : Set E<GOAL>Set.extremePoints 𝕜 ((convexHull 𝕜) A) ⊆ A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>s : Set E<GOAL>StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>h : StarConvex 𝕜 x s<VAR>y : E<VAR>hy : y ∈ s<GOAL>[x-[𝕜]y] ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>h : StarConvex 𝕜 x s<VAR>y : E<VAR>hy : y ∈ s<GOAL>openSegment 𝕜 x y ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>s : Set E<GOAL>StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<GOAL>StarConvex 𝕜 x ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<GOAL>StarConvex 𝕜 x Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 x t<GOAL>StarConvex 𝕜 x (s ∩ t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>S : Set (Set E)<VAR>h : ∀ s ∈ S, StarConvex 𝕜 x s<GOAL>StarConvex 𝕜 x (⋂₀ S)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>ι : Sort u_4<VAR>s : ι → Set E<VAR>h : ∀ (i : ι), StarConvex 𝕜 x (s i)<GOAL>StarConvex 𝕜 x (⋂ i, s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 x t<GOAL>StarConvex 𝕜 x (s ∪ t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>ι : Sort u_4<VAR>s : ι → Set E<VAR>hs : ∀ (i : ι), StarConvex 𝕜 x (s i)<GOAL>StarConvex 𝕜 x (⋃ i, s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x : E<VAR>S : Set (Set E)<VAR>hS : ∀ s ∈ S, StarConvex 𝕜 x s<GOAL>StarConvex 𝕜 x (⋃₀ S)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>SMul 𝕜 E<VAR>SMul 𝕜 F<VAR>x : E<VAR>y : F<VAR>s : Set E<VAR>t : Set F<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 y t<GOAL>StarConvex 𝕜 (x, y) (s ×ˢ t)
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>ι : Type u_4<VAR>E : ι → Type u_5<VAR>(i : ι) → AddCommMonoid (E i)<VAR>(i : ι) → SMul 𝕜 (E i)<VAR>x : (i : ι) → E i<VAR>s : Set ι<VAR>t : (i : ι) → Set (E i)<VAR>ht : ∀ ⦃i : ι⦄, i ∈ s → StarConvex 𝕜 (x i) (t i)<GOAL>StarConvex 𝕜 x (s.pi t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>h : s.Nonempty<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hx : x ∈ s<GOAL>StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hx : x ∈ s<GOAL>StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hx : x ∈ s<GOAL>StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<GOAL>StarConvex 𝕜 x {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>f : E →ₗ[𝕜] F<GOAL>StarConvex 𝕜 (f x) (⇑f '' s)