functor_map_eq_inf — Mathlib

English

If an open embedding is involved, applying the map to the functor yields the original open U.

Русский

При участии открывающего вложение отображение через map и functor возвращает исходное открытое множество U.

LaTeX

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

Lean4

@[simp]
theorem functor_map_eq_inf {X : TopCat} (U V : Opens X) :
    U.isOpenEmbedding.isOpenMap.functor.obj ((Opens.map U.inclusion').obj V) = V ⊓ U :=
  by
  ext1
  simp only [IsOpenMap.coe_functor_obj, map_coe, coe_inf, Set.image_preimage_eq_inter_range, set_range_inclusion' U]

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