inf_lt_inf_of_lt_of_sup_le_sup

Mathlib.Order.ModularLattice

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

English

If x < y and y ⊔ z ≤ x ⊔ z, then x ⊓ z < y ⊓ z in a modular lattice.

Русский

Если x < y и y ⊔ z ≤ x ⊔ z, то x ⊓ z < y ⊓ z в модульной решётке.

LaTeX

$$$ h_{xy} : x < y, hinf : y \\lor z \\le x \\lor z \\Rightarrow x \\land z < y \\land z $$$

Lean4

theorem inf_lt_inf_of_lt_of_sup_le_sup (hxy : x < y) (hinf : y ⊔ z ≤ x ⊔ z) : x ⊓ z < y ⊓ z :=
  sup_lt_sup_of_lt_of_inf_le_inf (α := αᵒᵈ) hxy hinf

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

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

Разделы

Аффилиация

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