basis_nhds — Mathlib

English

If f is inducing and 𝓝(f x) has a basis p with sets s, then 𝓝 x has basis p with preimages under f.

Русский

Если f индуцирующее и 𝓝(f x) имеет базис p на множествах s, то 𝓝 x имеет базис p на множимах-прообразах f.

LaTeX

$$$\operatorname{IsInducing}(f) \Rightarrow \forall x, (\mathcal{N}(f(x))).HasBasis\ p\ s \Rightarrow (\mathcal{N}(x)).HasBasis\ p\ (\mathrm{preimage}(f) \circ s).$$$

Lean4

theorem basis_nhds {p : ι → Prop} {s : ι → Set Y} (hf : IsInducing f) {x : X} (h_basis : (𝓝 (f x)).HasBasis p s) :
    (𝓝 x).HasBasis p (preimage f ∘ s) :=
  hf.nhds_eq_comap x ▸ h_basis.comap f

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