isCompl_ofDual_iff — Mathlib

English

Complementarity is preserved under the opposite of dual: IsCompl(ofDual a, ofDual b) iff IsCompl a b.

Русский

Комплементарность сохраняется при отражении двойственности: IsCompl(ofDual a, ofDual b) эквивалентно IsCompl a b.

LaTeX

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

Lean4

@[simp]
theorem isCompl_ofDual_iff {a b : αᵒᵈ} : IsCompl (ofDual a) (ofDual b) ↔ IsCompl a b :=
  ⟨IsCompl.dual, IsCompl.ofDual⟩

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