instInfSet

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#WithBot.instInfSet

English

Infimum structure on WithBot α is defined via the SupSet on the dual order: InfSet_{WithBot α} = WithTop.SupSet_{α^{op}}.

Русский

InfSet для WithBot α задаётся через SupSet для WithTop α^{op}.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru