mono

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Disjoint.mono

English

If a ≤ b and c ≤ d, then from Disjoint(b,d) we get Disjoint(a,c).

Русский

Если a ≤ b и c ≤ d, то из Disjoint(b,d) следует Disjoint(a,c).

LaTeX

$$$\\forall a,b,c,d\\, (a \\le b) \\to (c \\le d) \\to Disjoint(b,d) \\to Disjoint(a,c)$$$

Lean4

@[gcongr]
theorem mono (h₁ : a ≤ b) (h₂ : c ≤ d) : Disjoint b d → Disjoint a c := fun h _ ha hc ↦ h (ha.trans h₁) (hc.trans h₂)

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

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

Разделы

Аффилиация

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