sbtw_touchpoint_singleton — Mathlib

English

In a triangle t, the touchpoint with singleton {i2} lies strictly between t.points i3 and t.points i1.

Русский

В треугольнике t касательная точка с единичным {i2} лежит строго между t.points i3 и t.points i1.

LaTeX

$$$Sbtw_{\mathbb{R}}(t.touchpoint\{i_2\} i_2,\; t.points i_3,\; t.points i_1)$$$

Lean4

theorem sbtw_touchpoint_singleton {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
    Sbtw ℝ (t.points i₁) (t.touchpoint { i₂ } i₂) (t.points i₃) :=
  by
  rw [← t.mem_interior_face_iff_sbtw h₁₃]
  convert t.touchpoint_singleton_mem_interior_faceOpposite i₂
  rw [Affine.Simplex.faceOpposite]
  convert rfl using 2
  decide +revert

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