toDual_inf

Mathlib.Order.Lattice

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

English

In a min-ordered setting, the dual of infimum translates to the supremum in the dual.

Русский

В минимальном порядке переход к двойственности переводит наибольшее на противоположный порядок.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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