map_functor_eq' — Mathlib

English

Variant of the equality that the map functor returns V after applying the map to inclusion.

Русский

Вариант равенства: отображение функторa возвращает V после применения map к включению.

LaTeX

$$$ ((\mathrm{Opens.map} f).obj (hf.isOpenMap.functor.obj V)) = V $$$

Lean4

theorem map_functor_eq' {X U : TopCat} (f : U ⟶ X) (hf : IsOpenEmbedding f) (V) :
    ((Opens.map f).obj <| hf.isOpenMap.functor.obj V) = V :=
  Opens.ext <| Set.preimage_image_eq _ hf.injective

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