dual

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#IsCompl.dual

English

Dual of an IsCompl object maps to IsCompl in the dual setting: IsCompl x y → IsCompl (toDual x) (toDual y).

Русский

Двойственный образ IsCompl сохраняет IsCompl в двойственной задаче: IsCompl x y → IsCompl (toDual x) (toDual y).

LaTeX

$$$\text{IsCompl}(x,y) \rightarrow \text{IsCompl}(\text{toDual }x, \text{toDual }y)$$$

Lean4

theorem dual (h : IsCompl x y) : IsCompl (toDual x) (toDual y) :=
  ⟨h.2, h.1⟩

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

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

Разделы

Аффилиация

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