map_bihimp

Mathlib.Order.Heyting.Hom

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

English

In a Boolean algebra, the boundary of any element is the bottom element: ∂ a = ⊥.

Русский

В булевой алгебре граница любого элемента равна нулю: ∂ a = ⊥.

LaTeX

$$$ \partial a = \bot $$$

Lean4

@[simp]
theorem map_bihimp (a b : α) : f (a ⇔ b) = f a ⇔ f b := by simp_rw [bihimp, map_inf, map_himp]

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

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

Разделы

Аффилиация

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