le_total_of_codirected — Mathlib

English

Given two objects v1 and v2 both above a common r, either v1 ≤ v2 or v2 ≤ v1 holds.

Русский

Если оба v1, v2 выше общего r, то либо v1 ≤ v2, либо v2 ≤ v1.

LaTeX

$$$\forall r,v_1,v_2:\alpha,\ (r ≤ v_1) \land (r ≤ v_2) \Rightarrow (v_1 ≤ v_2) \lor (v_2 ≤ v_1)$$$

Lean4

theorem le_total_of_codirected {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) : v₁ ≤ v₂ ∨ v₂ ≤ v₁ :=
  by
  obtain ⟨n, rfl⟩ := h₁.exists_succ_iterate
  obtain ⟨m, rfl⟩ := h₂.exists_succ_iterate
  clear h₁ h₂
  wlog h : n ≤ m
  · rw [Or.comm]
    apply this
    exact Nat.le_of_not_ge h
  left
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  rw [Nat.add_comm, Function.iterate_add, Function.comp_apply]
  apply Order.le_succ_iterate

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