to_isWeakUpperModularLattice

Mathlib.Order.ModularLattice

URI: https://scilib.ai/kg/mathlib#IsUpperModularLattice.to_isWeakUpperModularLattice

English

Every IsUpperModularLattice is WeakUpperModularLattice.

Русский

Каждая IsUpperModularLattice является слабой верхней модульной.

LaTeX

$$$ \\text{If } \\alpha \\text{ is IsUpperModularLattice, then } \\alpha \\text{ is IsWeakUpperModularLattice.}$$$

Lean4

instance (priority := 100) to_isWeakUpperModularLattice : IsWeakUpperModularLattice α :=
  ⟨fun _ => CovBy.sup_of_inf_right⟩

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

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

Разделы

Аффилиация

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