isComplemented_iff — Mathlib

English

ComplementedLattice L iff every a ∈ L has a complement b ∈ L with IsCompl a b.

Русский

ComplementedLattice L эквивалентно каждому a ∈ L существует дополнение b ∈ L такое, что IsCompl a b.

LaTeX

$$ComplementedLattice L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b$$

Lean4

theorem isComplemented_iff : ComplementedLattice L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b :=
  by
  refine ⟨fun ⟨h⟩ a ha ↦ ?_, fun h ↦ ⟨fun ⟨a, ha⟩ ↦ ?_⟩⟩
  · obtain ⟨b, hb⟩ := h ⟨a, ha⟩
    exact ⟨b, b.property, CompleteSublattice.isCompl_iff.mp hb⟩
  · obtain ⟨b, hb, hb'⟩ := h a ha
    exact ⟨⟨b, hb⟩, CompleteSublattice.isCompl_iff.mpr hb'⟩

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