touchpoint_notMem_affineSpan_of_ne

English

If two vertex indices are different, the corresponding touchpoint cannot lie in the span of the opposite face.

Русский

Если i ≠ j, то точка касания по i не принадлежит аффинному пространству противоположной грани j.

LaTeX

$$$ (i \neq j) \Rightarrow s.touchpoint(\text{signs}, i) \notin \operatorname{affineSpan}_{\mathbb{R}}(\mathrm{Set.range}(s.faceOpposite(j).points)) $$$

Lean4

theorem touchpoint_notMem_affineSpan_of_ne {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs)
    {i j : Fin (n + 1)} (hne : i ≠ j) : s.touchpoint signs i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points) :=
  fun hm ↦
  h.touchpoint_injective.ne hne ((h.isTangentAt_touchpoint j).eq_of_mem_of_mem (h.touchpoint_mem_exsphere i) hm)

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