complementedLattice_iff — Mathlib

English

Iic(a) is a complemented lattice iff for every b ≤ a there exists c ≤ a with b ⊓ c = ⊥ and b ⊔ c = a.

Русский

Iic(a) является комплементированной решёткой тогда и только тогда, когда для каждого b ≤ a существует c ≤ a, такое что b ∧ c = ⊥ и b ∨ c = a.

LaTeX

$$$$\\text{ComplementedLattice}(\\mathrm{Iic}(a)) \\iff \\forall b \\le a\\;\\exists c \\le a,\\; b \\wedge c = \\bot \\land b \\vee c = a.$$$$

Lean4

protected theorem complementedLattice_iff [Lattice α] [OrderBot α] :
    ComplementedLattice (Iic a) ↔ ∀ b, b ≤ a → ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a := by
  simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff, exists_prop,
    Set.mem_Iic]

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