sdiff_idem

Mathlib.Order.Heyting.Basic

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

English

For all a,b in α, (a \ b) \ b = a \ b.

Русский

Для всех a,b ∈ α выполняется (a \ b) \ b = a \ b.

LaTeX

$$$ (a \backslash b) \backslash b = a \backslash b $$$

Lean4

@[simp]
theorem sdiff_idem : (a \ b) \ b = a \ b := by rw [sdiff_sdiff_left, sup_idem]

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

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

Разделы

Аффилиация

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