inf_left'

Mathlib.Order.Disjoint

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inf_left' (h : Disjoint a b) : Disjoint (c ⊓ a) b :=
  h.mono_left inf_le_right

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

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

Разделы

Аффилиация

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