interior_eq_image_Ioo — Mathlib

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]

Похожие утверждения