map_top

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.map_top

English

The comap of the top filter is the top filter: comap m ⊤ = ⊤.

Русский

Комап верхнего фильтра равен верхнему фильтру: comap m ⊤ = ⊤.

LaTeX

$$$\\mathrm{comap}\\ m\\ \\top = \\top$$$

Lean4

@[simp]
theorem map_top (f : α → β) : map f ⊤ = 𝓟 (range f) := by rw [← principal_univ, map_principal, image_univ]

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

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

Разделы

Аффилиация

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