mk' — Mathlib

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⟩

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