inclusion'_map_eq_top — Mathlib

English

The image of the top element under the functor induced by an open embedding equals the top open set.

Русский

Образ верхнего элемента через функтор открытого вложения равен верхнему открытым множествам.

LaTeX

$$$ U.isOpenEmbedding.isOpenMap.functor.obj \top = U $$$

Lean4

@[simp]
theorem inclusion'_map_eq_top {X : TopCat} (U : Opens X) : (Opens.map U.inclusion').obj U = ⊤ :=
  by
  ext1
  exact Subtype.coe_preimage_self _

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