isInducing_iff_nhds — Mathlib

English

An embedding-like property: IsInducing f is equivalent to nhds equality: ∀ x, nhds x = comap f (nhds (f x)).

Русский

Свойство индуцирования эквивалентно равенству окрестностей: ∀ x, nhds x = comap f (nhds (f x)).

LaTeX

$$$\operatorname{IsInducing}(f) \iff \forall x, \mathcal{N}_X(x) = \mathrm{comap}(f)(\mathcal{N}_Y(f(x))).$$$

Lean4

theorem isInducing_iff_nhds : IsInducing f ↔ ∀ x, 𝓝 x = comap f (𝓝 (f x)) :=
  (isInducing_iff _).trans (induced_iff_nhds_eq f)

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