complementedLattice_iff — Mathlib

English

β is complemented iff α is complemented, whenever α ≃o β.

Русский

β дополненная тогда и только тогда, когда α дополненная, если α и β изоморфны порядкам.

LaTeX

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

Lean4

theorem complementedLattice_iff (f : α ≃o β) : ComplementedLattice α ↔ ComplementedLattice β :=
  ⟨by intro; exact f.complementedLattice, by intro; exact f.symm.complementedLattice⟩

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