touchpoint_singleton_mem_interior_faceOpposite

English

Let s be a nondegenerate affine simplex and i an index. Then the touchpoint with singleton {i} lies in the interior of the opposite face:

Русский

Пусть s — невырожденный аффинный простейшн. Тогда касательная точка с единичным {i} принадлежитInterior противоположной грани.

LaTeX

$$$s.touchpoint\{i\} i \in \operatorname{Int}(s.faceOpposite(i))$$$

Lean4

theorem touchpoint_singleton_mem_interior_faceOpposite [Nat.AtLeastTwo n] (i : Fin (n + 1)) :
    s.touchpoint { i } i ∈ (s.faceOpposite i).interior :=
  by
  rw [faceOpposite, ← affineCombination_touchpointWeights,
    s.affineCombination_mem_interior_face_iff_pos _ (s.sum_touchpointWeights _ _)]
  simp only [Finset.mem_compl, Finset.mem_singleton, Decidable.not_not, forall_eq, touchpointWeights_eq_zero, and_true]
  intro j hj
  exact s.touchpointWeights_singleton_pos (Ne.symm hj)

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