of_disjoint_inf_of_le'

Mathlib.Order.Disjoint

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

English

If Disjoint (a ⊓ b) c and b ≤ c, then Disjoint a b.

Русский

Если Disjoint (a ⊓ b) c и b ≤ c, тогда Disjoint a b.

LaTeX

$$Disjoint (a \wedge b) c ∧ b ≤ c ⇒ Disjoint a b$$

Lean4

theorem of_disjoint_inf_of_le' (h : Disjoint (a ⊓ b) c) (hle : b ≤ c) : Disjoint a b :=
  disjoint_iff.2 <| h.eq_bot_of_le <| inf_le_of_right_le hle

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

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

Разделы

Аффилиация

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