English
Every proper cone naturally carries a pointed cone structure; specifically, there is a canonical coercion from a proper cone to a pointed cone.
Русский
Каждый правильный конус естественно получает структуру для точечного конуса; существует каноническое вложение из ProperCone в PointedCone.
LaTeX
$$$\text{toPointedCone} : ProperCone(R,E) \to\text{ PointedCone}(R,E)$$$
Lean4
/-- Two simplices glue nicely if the union of their vertices is affine independent. -/
theorem convexHull_inter (hs : AffineIndependent R ((↑) : s → E)) (ht₁ : t₁ ⊆ s) (ht₂ : t₂ ⊆ s) :
convexHull R (t₁ ∩ t₂ : Set E) = convexHull R t₁ ∩ convexHull R t₂ := by
classical
refine (Set.subset_inter (convexHull_mono inf_le_left) <| convexHull_mono inf_le_right).antisymm ?_
simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
rintro x ⟨⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩, w₂, -, h₂w₂, h₃w₂⟩
let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
replace hs :=
hs.eq_zero_of_sum_eq_zero_subtype h₁w <| by
simp only [w, sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂, sub_self]
have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
refine ⟨w₁, ?_, ?_, ?_⟩
· simp only [and_imp, Finset.mem_inter]
exact fun y hy₁ _ ↦ h₁w₁ y hy₁
all_goals
· rwa [sum_subset inter_subset_left]
rintro x
simp_intro hx₁ hx₂
simp [ht x hx₁ hx₂]
