English
If f is injective and for all x, comap f (𝓝 (f x)) = 𝓝 x, then f is an embedding.
Русский
Если отображение f инъективно и для всех x выполняется comap f (𝓝 (f x)) = 𝓝 x, то f является вложением.
LaTeX
$$$\forall x, \operatorname{comap} f (\mathcal{N}(f x)) = \mathcal{N}(x) \; \Rightarrow \; \mathrm{IsEmbedding}(f)$$$
Lean4
theorem mk' (f : X → Y) (inj : Injective f) (induced : ∀ x, comap f (𝓝 (f x)) = 𝓝 x) : IsEmbedding f :=
⟨isInducing_iff_nhds.2 fun x => (induced x).symm, inj⟩