isLUB_iff_le_iff — Mathlib

English

A is a least upper bound of s iff for every b, a ≤ b iff b is an upper bound of s.

Русский

Наименьшая верхняя грань a множества s эквивалентна тому, что для каждого b выполняется a ≤ b тогда и только если b — верхняя граница s.

LaTeX

$$$IsLUB(s,a) \\leftrightarrow (\\forall b, a \\le b \\leftrightarrow b \\in \\mathrm{upperBounds}(s))$$$

Lean4

theorem isLUB_iff_le_iff : IsLUB s a ↔ ∀ b, a ≤ b ↔ b ∈ upperBounds s :=
  ⟨fun h _ => isLUB_le_iff h, fun H => ⟨(H _).1 le_rfl, fun b hb => (H b).2 hb⟩⟩

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