map_coe

Mathlib.Topology.Category.TopCat.Opens

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

English

The underlying set of the mapped open (map f).obj U is exactly the preimage f^{-1}(U).

Русский

Множество-основание открытого множества, полученного через отображение, равно прообразу f^{-1}(U).

LaTeX

$$$((\\mathrm{map}\, f).\\mathrm{obj} U) = f^{-1}(U)$$$

Lean4

@[simp]
theorem map_coe (f : X ⟶ Y) (U : Opens Y) : ((map f).obj U : Set X) = f ⁻¹' (U : Set Y) :=
  rfl

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

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

Разделы

Аффилиация

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