instSemilatticeSup — Mathlib

English

The supremum operation on NonemptyCompacts is defined by taking the union of their underlying compact sets.

Русский

Операция взятия наибольшего (sup) над не пустыми компактами определяется как объединение их подлежащих компактных множеств.

LaTeX

$$$ (K \mathrm{max} L : \mathrm{Set}\,\alpha) = K \cup L $$$

Lean4

instance : SemilatticeSup (NonemptyCompacts α) :=
  SetLike.coe_injective.semilatticeSup _ fun _ _ => rfl

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