le_sdiff_sup

Mathlib.Order.Heyting.Basic

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

English

a ≤ (a \\ b) ∪ b

Русский

a ≤ (a \\ b) ∪ b.

LaTeX

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

Lean4

theorem le_sdiff_sup : a ≤ a \ b ⊔ b := by rw [sup_comm, ← sdiff_le_iff]

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

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

Разделы

Аффилиация

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