le_sSup — Mathlib

English

If a is an atom, then a ≤ sSup s iff there exists b in s with a ≤ b.

Русский

Если a — атом, то a ≤ sSup(s) тогда и только тогда, когда существует b в s such that a ≤ b.

LaTeX

$$$ \\mathrm{IsAtom}(a) \\rightarrow \\bigl( a \\le \\mathrm{sSup}(s) \\iff \\exists b \\in s,\\ a \\le b \\bigr)$$$

Lean4

protected theorem le_sSup (ha : IsAtom a) : a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b := by simp [sSup_eq_iSup', ha.le_iSup]

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