le_sup_sdiff_sup_sdiff

Mathlib.Order.Heyting.Basic

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

English

a ≤ b ⊔ (a \\ c ⊔ c \\ b).

Русский

a ≤ b ⊔ (a \\ c ⊔ c \\ b).

LaTeX

$$$a \\le b \\sqcup (a \\setminus c \\sqcup c \\setminus b)$$$

Lean4

@[simp]
theorem le_sup_sdiff_sup_sdiff : a ≤ b ⊔ (a \ c ⊔ c \ b) := by simpa using @sdiff_sdiff_sdiff_le_sdiff

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

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

Разделы

Аффилиация

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