map_sdiff'

Mathlib.Order.Hom.BoundedLattice

URI: https://scilib.ai/kg/mathlib#map_sdiff'

← MathLib Explorer

English

Boolean-algebra homomorphisms preserve set-difference: f(a \ b) = f(a) \ f(b).

Русский

Гомоморфизм булевой алгебры сохраняет разность: f(a \ b) = f(a) \ f(b).

LaTeX

$$$f(a \ b) = f(a) \ f(b)$$$

Lean4

/-- Special case of `map_sdiff` for Boolean algebras. -/
theorem map_sdiff' (a b : α) : f (a \ b) = f a \ f b := by rw [sdiff_eq, sdiff_eq, map_inf, map_compl']

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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