sdiff_sup_sdiff_cancel

Mathlib.Order.Heyting.Basic

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

← MathLib Explorer

English

Let hba hold: b ≤ a and hcb: c ≤ b. Then a \\ b ⊔ b \\ c = a \\ c.

Русский

Пусть b ≤ a и c ≤ b. Тогда a \\ b ⊔ b \\ c = a \\ c.

LaTeX

$$$ a \\\\setminus b \\\\sqcup b \\\\setminus c = a \\\\setminus c $$$

Lean4

theorem sdiff_sup_sdiff_cancel (hba : b ≤ a) (hcb : c ≤ b) : a \ b ⊔ b \ c = a \ c :=
  (sdiff_triangle _ _ _).antisymm' <| sup_le (sdiff_le_sdiff_left hcb) (sdiff_le_sdiff_right hba)

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

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

Разделы

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

Аффилиация

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