sdiff_le_sdiff

Mathlib.Order.Heyting.Basic

URI: https://scilib.ai/kg/mathlib#sdiff_le_sdiff

English

With a pair of inequalities a ≤ b and c ≤ d, we have a \ d ≤ b \ c.

Русский

С параллелем неравенств a ≤ b и c ≤ d имеем a \ d ≤ b \ c.

LaTeX

$$$\forall a,b,c,d:\alpha,\; a \ d \le b \ c$$$

Lean4

@[gcongr]
theorem sdiff_le_sdiff (hab : a ≤ b) (hcd : c ≤ d) : a \ d ≤ b \ c :=
  (sdiff_le_sdiff_right hab).trans <| sdiff_le_sdiff_left hcd

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

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

Разделы

Аффилиация

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