wbtw_or_wbtw_or_wbtw — Mathlib

English

If {x, y, z} is collinear, then one of the cyclic weak betweenness relations holds among the three points.

Русский

Если {x, y, z} лежат на одной прямой, тогда одном из циклических отношений слабого между выполняется между.

LaTeX

$$$\text{Collinear}(R, {x,y,z}) \Rightarrow (Wbtw_R x y z \lor Wbtw_R y z x \lor Wbtw_R z x y)$$$

Lean4

theorem wbtw_or_wbtw_or_wbtw {x y z : P} (h : Collinear R ({ x, y, z } : Set P)) :
    Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y :=
  by
  rw [collinear_iff_of_mem (Set.mem_insert _ _)] at h
  rcases h with ⟨v, h⟩
  simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at h
  have hy := h y (Or.inr (Or.inl rfl))
  have hz := h z (Or.inr (Or.inr rfl))
  rcases hy with ⟨ty, rfl⟩
  rcases hz with ⟨tz, rfl⟩
  rcases lt_trichotomy ty 0 with (hy0 | rfl | hy0)
  · rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)
    · rw [wbtw_comm (z := x)]
      rw [← or_assoc]
      exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonpos _ _ hy0.le hz0.le)
    · simp
    · exact Or.inr (Or.inr (wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos _ _ hz0.le hy0.le))
  · simp
  · rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)
    · refine Or.inr (Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg _ _ hz0.le hy0.le))
    · simp
    · rw [wbtw_comm (z := x)]
      rw [← or_assoc]
      exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonneg _ _ hy0.le hz0.le)

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