English
Let s be a nondegenerate affine simplex in a Euclidean space. Then for every i among the vertices, the touchpoint corresponding to the empty set lies in the interior of the opposite face:
Русский
Пусть s — невырожденный аффинный n–Simplex. Тогда для каждого i касательная точка, соответствующая пустому множеству, принадлежит Interior противоположной грани к вершине i.
LaTeX
$$$s.touchpoint\,\emptyset\,i \in \operatorname{Int}(s.faceOpposite(i))$$$
Lean4
theorem touchpoint_empty_mem_interior_faceOpposite [Nat.AtLeastTwo n] (i : Fin (n + 1)) :
s.touchpoint ∅ 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_empty_pos (Ne.symm hj)
