inl — Mathlib

English

For x ∈ X, the neighborhood filter at inl(x) is the image of the neighborhood filter at x under the left injection.

Русский

Для x ∈ X фильтр окрестностей в точке inl(x) равен образу фильтра окрестностей в x через левую вложение.

LaTeX

$$$\\nhds(\\\\mathrm{inl}(x)) = (\\\\mathrm{map}\\;\\\\mathrm{inl})(\\nhds x)$$$

Lean4

protected theorem inl : IsOpenEmbedding (@inl X Y) :=
  .of_continuous_injective_isOpenMap continuous_inl inl_injective isOpenMap_inl

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