map_obj

Mathlib.Topology.Category.TopCat.OpenNhds

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.OpenNhds.map_obj

English

The map on OpenNhds objects respects the underlying open sets under the open map f.

Русский

Отображение на объектах OpenNhds сохраняет открытые множества под открытым отображением f.

LaTeX

$$map_obj (x) (U) (q) : (map f x).obj ⟨U, q⟩ = ⟨(Opens.map f).obj U, q⟩$$

Lean4

@[simp]
theorem map_obj (x : X) (U) (q) : (map f x).obj ⟨U, q⟩ = ⟨(Opens.map f).obj U, q⟩ :=
  rfl

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

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

Разделы

Аффилиация

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