isLUB_le_iff — Mathlib

English

If s has a least upper bound a, then for every b, a ≤ b iff b is an upper bound of s.

Русский

Если множество s имеет наименьшую верхнюю грань a, то для каждого b верно: a ≤ b тогда и только если b является верхней границей s.

LaTeX

$$$IsLUB(s,a) \\rightarrow (a \\le b \\iff b \\in \\mathrm{upperBounds}(s))$$$

Lean4

theorem isLUB_le_iff (h : IsLUB s a) : a ≤ b ↔ b ∈ upperBounds s :=
  by
  rw [h.upperBounds_eq]
  rfl

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