sbtw_touchpoint_empty — Mathlib

English

In a triangle formed by the points of t with indices i1, i2, i3, the touchpoint corresponding to the empty set lies strictly between the two vertex points:

Русский

В треугольнике с вершинами t.points i1, t.points i2, t.points i3 касательная точка, соответствующая пустому набору, лежит строго между двумя вершинами.

LaTeX

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

Lean4

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

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