toDual_sup

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#toDual_sup

English

The dual of supremum equals the infimum in the dual: toDual(a ⊔ b) = toDual a ⊓ toDual b.

Русский

Двойственный верхний предел равен нижнему в двойственном порядке: toDual(a ⊔ b) = toDual a ⊓ toDual b.

LaTeX

$$$ toDual(a \sqcup b) = toDual(a) \sqcap b$$$

Lean4

@[simp]
theorem toDual_sup [Max α] (a b : α) : toDual (a ⊔ b) = toDual a ⊓ toDual b :=
  rfl

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

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

Разделы

Аффилиация

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