lt_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lt_iff (h : IsLeast s a) : b < a ↔ ∀ x ∈ s, b < x :=
  h.dual.lt_iff

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