complementedLattice — Mathlib

English

If α is a complemented lattice and f: α ≃o β, then β is also a complemented lattice.

Русский

Если α — дополненная решетка и есть изоморфизм порядка f: α ≃o β, то β тоже дополненная решетка.

LaTeX

$$$ \text{ComplementedLattice}(\beta) $$$

Lean4

theorem complementedLattice [ComplementedLattice α] (f : α ≃o β) : ComplementedLattice β :=
  ⟨fun x => by
    obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)
    rw [← f.symm_apply_apply y] at hy
    exact ⟨f y, f.symm.isCompl_iff.2 hy⟩⟩

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