supSet — Mathlib

English

For posets α and β with SupSet structure, the supremum set in α×β is obtained componentwise from the supremums in α and β: SupSet(α×β) s = (sSup fst''s, sSup snd''s).

Русский

Для частично упорядоченных множеств α и β с структурой верхних граней верхний набор в произведении α×β задаётся по компонентам: SupSet(α×β) s = (sup fst''s, sup snd''s).

LaTeX

$$$[SupSet\ α][SupSet\ β] \to\ SupSet(\mathrm{Prod}\ α β): s \mapsto (sSup (\mathrm{fst}'' s),\ sSup (\mathrm{snd}'' s))$$$

Lean4

instance supSet [SupSet α] [SupSet β] : SupSet (α × β) :=
  ⟨fun s => (sSup (Prod.fst '' s), sSup (Prod.snd '' s))⟩

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