map_compl'

Mathlib.Order.Hom.BoundedLattice

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

English

A Boolean algebra homomorphism preserves complementation on elements: f(aᶜ) = (f(a))ᶜ.

Русский

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

LaTeX

$$$f(a^{c}) = (f(a))^{c}$$$

Lean4

/-- Special case of `map_compl` for Boolean algebras. -/
theorem map_compl' (a : α) : f aᶜ = (f a)ᶜ :=
  (isCompl_compl.map _).compl_eq.symm

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

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

Разделы

Аффилиация

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