sdiff_le_sdiff_of_sup_le_sup_left

Mathlib.Order.Heyting.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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