map_compl

Mathlib.Order.Heyting.Hom

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

English

A function f between Heyting algebras preserves the complement: f(aᶜ) = (f a)ᶜ.

Русский

Функция между Хейтинговыми алгебрами сохраняет complément: f(aᶜ) = (f a)ᶜ.

LaTeX

$$$ f(a^{\complement}) = (f a)^{\complement} $$$

Lean4

@[simp]
theorem map_compl (a : α) : f aᶜ = (f a)ᶜ := by rw [← himp_bot, ← himp_bot, map_himp, map_bot]

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

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

Разделы

Аффилиация

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