csSup_le_csSup — Mathlib

English

Let α be a ConditionallyCompleteLattice. If t bounds s from above and s is nonempty, and s ⊆ t, then sSup(s) ≤ sSup(t).

Русский

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

LaTeX

$$$(t \text{ bounded above}) \land s \neq \varnothing \land (s \subseteq t) \rightarrow \mathrm{sSup}(s) \le \mathrm{sSup}(t)$$$

Lean4

@[gcongr low]
theorem csSup_le_csSup (ht : BddAbove t) (hs : s.Nonempty) (h : s ⊆ t) : sSup s ≤ sSup t :=
  csSup_le hs fun _ ha => le_csSup ht (h ha)

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