sdiff_sup_self

Mathlib.Order.Heyting.Basic

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

English

b \\ a ⊔ a = b ⊔ a.

Русский

b \\ a ⊔ a = b ⊔ a.

LaTeX

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

Lean4

@[simp]
theorem sdiff_sup_self (a b : α) : b \ a ⊔ a = b ⊔ a := by rw [sup_comm, sup_sdiff_self, sup_comm]

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

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

Разделы

Аффилиация

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