covBy_sup_of_inf_covBy_left

Mathlib.Order.ModularLattice

URI: https://scilib.ai/kg/mathlib#covBy_sup_of_inf_covBy_left

English

In a lattice with IsUpperModularLattice, if a ∧ b ⋖ a then b ⋖ a ∨ b.

Русский

В решётке с IsUpperModularLattice, если a ∧ b ⋖ a, то b ⋖ a ∨ b.

LaTeX

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

Lean4

theorem covBy_sup_of_inf_covBy_left : a ⊓ b ⋖ a → b ⋖ a ⊔ b :=
  IsUpperModularLattice.covBy_sup_of_inf_covBy

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru