isCompl_sup_left_of_isCompl_sup_right

English

From modularity one derives a lower modular law for the lattice, giving a compatibility condition with infimum and supremum.

Русский

Из модульности следует нижняя модульная лемма, обеспечивающая совместимость операций infimum и supremum.

LaTeX

$$$\text{IsLowerModularLattice }\alpha$ with the modular law: \forall a,b,c, a\vee b ⩽ c \Rightarrow \cdots$$$

Lean4

theorem isCompl_sup_left_of_isCompl_sup_right [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Disjoint b c)
    (hcomp : IsCompl a (b ⊔ c)) : IsCompl (a ⊔ b) c :=
  ⟨h.disjoint_sup_left_of_disjoint_sup_right hcomp.disjoint, codisjoint_assoc.mpr hcomp.codisjoint⟩

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