preimage_mem_nhds — Mathlib

English

If f is continuous at x and t is a neighborhood of f(x), then the preimage f^{-1}(t) is a neighborhood of x.

Русский

Если f непрерывна в x и t ∈ 𝓝(f(x)), то f^{-1}(t) является окрестностью x.

LaTeX

$$$\\mathrm{ContinuousAt}(f, x) \\Rightarrow t \\in 𝓝(f(x)) \\Rightarrow f^{-1}(t) \\in 𝓝(x)$$$

Lean4

theorem preimage_mem_nhds {t : Set Y} (h : ContinuousAt f x) (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝 x :=
  h ht

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