instSemilatticeSup — Mathlib

English

There is a Max (join) operation on PositiveCompacts α induced by union of underlying sets, preserving nonemptiness.

Русский

Существует операция максимума (⊔) на PositiveCompacts α, индуцированная объединением носителей, сохраняющая непустость.

LaTeX

$$$ \text{instance } \text{Max}(\mathrm{PositiveCompacts}\, \alpha) \;,$$$

Lean4

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

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