isOpenEmbedding_obj_top — Mathlib

English

In a functor from Opens X to Opens Y, the map on objects is injective when there is a dominating property.

Русский

Для функторирования между Opens, отображение объектов инъективно при наличии определенного доминирующего свойства.

LaTeX

$$$ hf.functor.obj \; \text{ is injective.}$$$

Lean4

@[simp]
theorem isOpenEmbedding_obj_top {X : TopCat} (U : Opens X) : U.isOpenEmbedding.isOpenMap.functor.obj ⊤ = U :=
  by
  ext1
  exact Set.image_univ.trans Subtype.range_coe

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