inclusion_obj

Mathlib.Topology.Category.TopCat.OpenNhds

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

English

The inclusion functor preserves objects, sending the structured object ⟨U, p⟩ to U.

Русский

Функтор включения сохраняет объекты, переводя структуру ⟨U, p⟩ в U.

LaTeX

$$inclusion_obj (x) (U) (p) : (inclusion x).obj ⟨U, p⟩ = U$$

Lean4

@[simp]
theorem inclusion_obj (x : X) (U) (p) : (inclusion x).obj ⟨U, p⟩ = U :=
  rfl

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

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

Разделы

Аффилиация

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