map_top

Mathlib.Topology.Category.TopCat.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.map_top

English

The image of the top open under map f is the top open: (Opens.map f).obj ⊤ = ⊤.

Русский

Образ верхнего открытого множества под отображением f есть верхнее открытое множество: (Opens.map f).obj ⊤ = ⊤.

LaTeX

$$$(\\mathrm{Opens.map}\\ f).\\mathrm{obj} \\top = \\top$$$

Lean4

@[simp]
theorem map_top (f : X ⟶ Y) : (Opens.map f).obj ⊤ = ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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