le_of_not_gt — Mathlib

English

If s is a chain under a preorder 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 < y \\rightarrow y \\le x $$$

Lean4

theorem le_of_not_gt [Preorder α] (hs : IsChain (· ≤ ·) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬x < y) : y ≤ x :=
  by
  cases hs.total hx hy with
  | inr h' => exact h'
  | inl h' => simpa [lt_iff_le_not_ge, h'] using h

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