instSupSet — Mathlib

English

The supremum-collection on WithBot α is defined via the InfSet on the dual order: SupSet_{WithBot α} = WithTop.InfSet_{α^{op}}.

Русский

Обозначение SUPSet для WithBot α задаётся через InfSet для WithTop α^{op}.

LaTeX

$$$$ \operatorname{SupSet}_{WithBot \ α} = ( \operatorname{WithTop}._{α^{op}} ).\operatorname{InfSet}. $$$$

Lean4

noncomputable instance instSupSet [SupSet α] : SupSet (WithBot α) :=
  ⟨(WithTop.instInfSet (α := αᵒᵈ)).sInf⟩

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