not_lt — Mathlib

English

In a chain, not x < y is equivalent to y ≤ x for x,y ∈ s.

Русский

В цепи Not (x < y) эквивалентно y ≤ x для x,y ∈ s.

LaTeX

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

Lean4

theorem not_lt [Preorder α] (hs : IsChain (· ≤ ·) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : ¬x < y ↔ y ≤ x :=
  ⟨(hs.le_of_not_gt hx hy ·), fun h h' ↦ h'.not_ge h⟩

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