isEmbedding — Mathlib

English

Let f be an open embedding. Then the image of the neighborhood filter at x equals the neighborhood filter at f(x): map f (𝓝 x) = 𝓝 (f x).

Русский

Пусть f — открытое вложение. Тогда образ фильтра окрестностей x равен фильтру окрестностей f(x): map f (𝓝 x) = 𝓝 (f x).

LaTeX

$$$ \operatorname{map} f (\mathcal{N}(x)) = \mathcal{N}(f(x)) $$$

Lean4

theorem isEmbedding (hf : IsOpenEmbedding f) : IsEmbedding f :=
  hf.toIsEmbedding

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