sdiff_sdiff_right_self

Mathlib.Order.BooleanAlgebra.Basic

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

English

For any x, y in a generalized boolean algebra, x \ (x \ y) = x ⊓ y.

Русский

Для любых x, y в обобщённой булевой алгебре выполняется x \ (x \ y) = x ⊓ y.

LaTeX

$$$$ x \setminus (x \setminus y) = x \wedge y $$$$

Lean4

@[simp]
theorem sdiff_sdiff_right_self : x \ (x \ y) = x ⊓ y := by rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]

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

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

Разделы

Аффилиация

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