inf_right'

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Disjoint.inf_right'

English

If a ⊓ b = ⊥, then Disjoint a (c ⊓ b) for all c.

Русский

Если a ⊓ b = ⊥, то Disjoint a (c ⊓ b) для любого c.

LaTeX

$$Disjoint a b → ∀ c, Disjoint a (c ∧ b)$$

Lean4

theorem inf_right' (h : Disjoint a b) : Disjoint a (c ⊓ b) :=
  h.mono_right inf_le_right

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

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

Разделы

Аффилиация

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