csSup_insert — Mathlib

English

The supremum of insert a s is the maximum of a and the supremum of s, provided s is nonempty and bounded above.

Русский

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

LaTeX

$$$\forall s:\\text{Set }\alpha,\forall a:\\alpha,\ BddAbove\ s \\to s.Nonempty \\to sSup(\text{insert } a\ s) = a \sqcup sSup s$$$

Lean4

/-- The supremum of `insert a s` is the maximum of `a` and the supremum of `s`, if `s` is
nonempty and bounded above. -/
@[simp]
theorem csSup_insert (hs : BddAbove s) (sne : s.Nonempty) : sSup (insert a s) = a ⊔ sSup s :=
  ((isLUB_csSup sne hs).insert a).csSup_eq (insert_nonempty a s)

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