comap_top

Mathlib.Order.BooleanSubalgebra

URI: https://scilib.ai/kg/mathlib#BooleanSubalgebra.comap_top

English

The comap of the top subalgebra along f is the top subalgebra: ⊤.comap f = ⊤.

Русский

Обратное образование верхней подалгебры вдоль f равно верхней: ⊤.comap f = ⊤.

LaTeX

$$$(\top : BooleanSubalgebra\ β).comap f = \top$$$

Lean4

@[simp]
theorem comap_top (f : BoundedLatticeHom α β) : (⊤ : BooleanSubalgebra β).comap f = ⊤ :=
  (gc_map_comap f).u_top

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

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

Разделы

Аффилиация

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