isCompl_inf_inf_of_isCompl_of_le — Mathlib

English

In a bounded modular lattice, the diamond between Iic and Ici intervals yields complementariness relations.

Русский

В ограниченной модульной решётке диамант между интервалами Iic и Ici задаёт отношения дополнимости.

LaTeX

$$$IicOrderIsoIci(a,b):\; Set.Iic a \simeq_o Set.Ici b$ (via diamond isomorphism).$$

Lean4

theorem isCompl_inf_inf_of_isCompl_of_le [Lattice α] [BoundedOrder α] [IsModularLattice α] {a b c : α}
    (h₁ : IsCompl b c) (h₂ : b ≤ a) : IsCompl (⟨a ⊓ b, inf_le_left⟩ : Iic a) (⟨a ⊓ c, inf_le_left⟩ : Iic a) :=
  by
  constructor
  · simp [disjoint_iff, Subtype.ext_iff, inf_comm a c, inf_assoc a, ← inf_assoc b, h₁.inf_eq_bot]
  · simp only [Iic.codisjoint_iff, inf_comm a, IsModularLattice.inf_sup_inf_assoc]
    simp [inf_of_le_left h₂, h₁.sup_eq_top]

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