touchpoint_empty_notMem_affineSpan_of_ne

English

Along a line from the excenter through the touchpoint, the sign of the signed distance remains constant for r in [0,1].

Русский

Для линейного отображения через эксцентр и точку касания, знак signedInfDist по j-го индекса на отображении равен знаку на эксцентре для r в [0,1].

LaTeX

$$$ SignType.sign\left( s.signedInfDist_j\left(\mathrm{AffineMap.lineMap}(s.excenter, s.touchpoint(i), r)\right)\right) = SignType.sign\left( s.signedInfDist_j( s.excenter ) \right) \quad (r \in [0,1]) $$$

Lean4

theorem touchpoint_empty_notMem_affineSpan_of_ne {i j : Fin (n + 1)} (hne : i ≠ j) :
    s.touchpoint ∅ i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points) :=
  s.excenterExists_empty.touchpoint_notMem_affineSpan_of_ne hne

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