sdiff_le_sdiff_of_sup_le_sup_right

Mathlib.Order.Heyting.Basic

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

← MathLib Explorer

English

If h : a ⊔ c ≤ b ⊔ c, then a \\ c ≤ b \\ c.

Русский

Если h : a ⊔ c ≤ b ⊔ c, то a \\ c ≤ b \\ c.

LaTeX

$$$ a \\\\setminus c \\\\le b \\\\setminus c $$$

Lean4

theorem sdiff_le_sdiff_of_sup_le_sup_right (h : a ⊔ c ≤ b ⊔ c) : a \ c ≤ b \ c :=
  by
  rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]
  exact sdiff_le_sdiff_right h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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