English
The closed interior of a 1-simplex is exactly the segment joining its two vertices.
Русский
Замкнутая внутренняя часть 1-кона — это точно отрезок между двумя вершинами.
LaTeX
$$$s.closedInterior = \\ affineSegment_R( s.points 0, s.points 1)$$$
Lean4
/-- The closed interior of a 1-simplex is a segment between its vertices. -/
theorem closedInterior_eq_affineSegment (s : Simplex R P 1) :
s.closedInterior = affineSegment R (s.points 0) (s.points 1) :=
by
ext p
constructor
· rintro ⟨w, hw, h01, rfl⟩
have h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1) :=
by
rw [Fin.sum_univ_two] at hw
ext i
fin_cases i <;> simp [← hw]
rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _)]
exact Set.mem_image_of_mem _ (h01 _)
· rintro ⟨r, ⟨h0, h1⟩, rfl⟩
rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _),
affineCombination_mem_closedInterior_iff
(Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]
intro i
fin_cases i <;> simp [h0, h1]
