English
The interior of a 1-simplex is the image of the open interval under the affine line map from the first to the second vertex.
Русский
Внутренняя часть 1-кона есть образ открытого отрезка под аффинной линией, соединяющей две вершины.
LaTeX
$$s.interior = AffineMap.lineMap (s.points 0) (s.points 1) '' Set.Ioo (0 : R) 1$$
Lean4
/-- The interior of a 1-simplex is a segment between its vertices. -/
theorem interior_eq_image_Ioo (s : Simplex R P 1) :
s.interior = AffineMap.lineMap (s.points 0) (s.points 1) '' Set.Ioo (0 : R) 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_interior_iff
(Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]
intro i
fin_cases i <;> simp [h0, h1]