lt_iff — Mathlib

English

If s has a greatest element a, then for any b, a < b iff every x in s satisfies x < b.

Русский

Если у s есть наибольший элемент a, то для любого b верно: a < b тогда и только если для всех x ∈ s выполняется x < b.

LaTeX

$$$IsGreatest(s,a) \\rightarrow (a < b \\iff \\forall x \\in s, x < b)$$$

Lean4

theorem lt_iff (h : IsGreatest s a) : a < b ↔ ∀ x ∈ s, x < b :=
  ⟨fun hlt _x hx => (h.2 hx).trans_lt hlt, fun h' => h' _ h.1⟩

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