lt_of_not_ge — Mathlib

English

If s is a chain and x,y ∈ s with not x ≤ y, then y < x.

Русский

Если s — цепь и x,y ∈ s и не x ≤ y, тогда y < x.

LaTeX

$$$ IsChain\\ (\\le)\\ s \\rightarrow x \\in s \\rightarrow y \\in s \\rightarrow \\neg x \\le y \\rightarrow y < x $$$

Lean4

theorem lt_of_not_ge [Preorder α] (hs : IsChain (· ≤ ·) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬x ≤ y) : y < x :=
  (hs.total hx hy).elim (h · |>.elim) (lt_of_le_not_ge · h)

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