inf_covBy_of_covBy_sup_of_covBy_sup_left

English

In a lattice with IsWeakLowerModularLattice, if a ≤ a ∨ b is covered by a and b covers a ∨ b, then a ∧ b covers a.

Русский

В решётке с IsWeakLowerModularLattice, если a ⩽ a ∨ b покрывает a, и b покрывает a ∨ b, то a ∧ b покрывает a.

LaTeX

$$$ a \\_\\triangleleft a \\vee b \\rightarrow b \\triangleleft a \\vee b \\rightarrow a \\wedge b \\triangleleft a $$$

Lean4

theorem inf_covBy_of_covBy_sup_of_covBy_sup_left : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a :=
  IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup

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