map_functor_eq — Mathlib

English

Let i: U ↪ X be the inclusion of an open subset U of a topological space X. For every open V ⊆ U, the induced map on opens takes V to itself.

Русский

Пусть i: U ↪ X — включение открытого подмножества U в X. Для любого открытого V ⊆ U образ по индуцированному отображению открытых множеств равен V.

LaTeX

$$$ i_{*}(V) = V \\quad \\text{for all } V \\in \\mathrm{Op}(U). $$$

Lean4

@[simp]
theorem map_functor_eq {X : TopCat} {U : Opens X} (V : Opens U) :
    ((Opens.map U.inclusion').obj <| U.isOpenEmbedding.isOpenMap.functor.obj V) = V :=
  TopologicalSpace.Opens.map_functor_eq' _ U.isOpenEmbedding V

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