mono_left

Mathlib.Order.Disjoint

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

English

If a ≤ b, then Disjoint b c implies Disjoint a c.

Русский

Если a ≤ b, то Disjoint b c => Disjoint a c.

LaTeX

$$$Disjoint(mono\\_left)(\\,h\\:a\\le b\\,)\\; :\\; Disjoint b c \\to Disjoint a c$$$

Lean4

theorem mono_left (h : a ≤ b) : Disjoint b c → Disjoint a c :=
  Disjoint.mono h le_rfl

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

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

Разделы

Аффилиация

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