le_csSup_of_le — Mathlib

English

Let α be a ConditionallyCompleteLattice. If s is a subset of α that is bounded above, and b is an element of s with a ≤ b, then a ≤ sSup(s).

Русский

Пусть α — условно полноупорядоченная решетка. Пусть s ⊆ α ограничено сверху, и существует b ∈ s такой, что a ≤ b. Тогда a ≤ sSup(s).

LaTeX

$$$BddAbove(s) \land b \in s \land a \le b \rightarrow a \le \mathrm{sSup}(s)$$$

Lean4

theorem le_csSup_of_le (hs : BddAbove s) (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s :=
  le_trans h (le_csSup hs hb)

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