ωSup_total — Mathlib

English

If for every i, c(i) ≤ x or x ≤ c(i), then either ωSup c ≤ x or x ≤ ωSup c.

Русский

Если для каждого i выполняется c(i) ≤ x или x ≤ c(i), то либо ωSup c ≤ x, либо x ≤ ωSup c.

LaTeX

$$$$ \forall c : \text{Chain }\alpha, \forall x \in \alpha, \Big( \forall i, c(i) \le x \lor x \le c(i) \Big) \Rightarrow \omegaSup c \le x \lor x \le \omegaSup c. $$$$

Lean4

theorem ωSup_total {c : Chain α} {x : α} (h : ∀ i, c i ≤ x ∨ x ≤ c i) : ωSup c ≤ x ∨ x ≤ ωSup c :=
  by_cases (fun (this : ∀ i, c i ≤ x) => Or.inl (ωSup_le _ _ this))
    (fun (this : ¬∀ i, c i ≤ x) =>
      have : ∃ i, ¬c i ≤ x := by simp only [not_forall] at this ⊢; assumption
      let ⟨i, hx⟩ := this
      have : x ≤ c i := (h i).resolve_left hx
      Or.inr <| le_ωSup_of_le _ this)

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