instOrderDual

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#ComplementedLattice.instOrderDual

English

The dual of a complemented lattice is complemented.

Русский

Двойственная по порядку структура комплементированная.

LaTeX

$$$ComplementedLattice( OrderDual(\\alpha) )$$$

Lean4

instance : ComplementedLattice αᵒᵈ :=
  ⟨fun a ↦
    let ⟨b, hb⟩ := exists_isCompl (show α from a)
    ⟨b, hb.dual⟩⟩

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

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

Разделы

Аффилиация

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