isCompl

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderIso.isCompl

English

An order isomorphism maps complements: if IsCompl x y in α, then IsCompl (f x) (f y) in β.

Русский

Изоморфизм порядка переводит пары дополнений: если IsCompl x y в α, то IsCompl(f x) (f y) в β.

LaTeX

$$$ IsCompl(x,y) \Rightarrow IsCompl(f(x), f(y)) $$$

Lean4

theorem isCompl {x y : α} (h : IsCompl x y) : IsCompl (f x) (f y) :=
  ⟨h.1.map_orderIso _, h.2.map_orderIso _⟩

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

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

Разделы

Аффилиация

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