ofDual — Mathlib

English

If a and b are complements in the dual order αᵒᵈ, then ofDual(a) and ofDual(b) are complements in α.

Русский

Если элементы a и b являются комплементами в двойственном порядке αᵒᵈ, то их образы под отображением ofDual являются комплементами в α.

LaTeX

$$$$ IsCompl(a,b) \rightarrow IsCompl(\mathrm{ofDual}(a), \mathrm{ofDual}(b)). $$$$

Lean4

theorem ofDual {a b : αᵒᵈ} (h : IsCompl a b) : IsCompl (ofDual a) (ofDual b) :=
  ⟨h.2, h.1⟩

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