covBy_sup_of_inf_covBy_of_inf_covBy_right

English

In a lattice with weak lower modularity, if a ∧ b and b cover b? the dual statement: If a ∧ b is covered by a or by b, then b covers a ∨ b.

Русский

В решётке со слабой нижней модульностью, если a ∧ b покрывает b? двойственный вариант, если a ∧ b покрывает a или b, тогда b покрывает a ∨ b.

LaTeX

$$$ a \\wedge b \\; \\prec\\; a \\\\Rightarrow a \\wedge b \\; \\prec\\; b \\Rightarrow b \\; \\prec\\; a \\vee b $$$

Lean4

theorem covBy_sup_of_inf_covBy_of_inf_covBy_right : a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b :=
  by
  rw [inf_comm, sup_comm]
  exact fun ha hb => covBy_sup_of_inf_covBy_of_inf_covBy_left hb ha

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