preimage_mem_nhdsWithin — Mathlib

English

If f is continuous within s at x and t ∈ nhds (f x), then f⁻¹' t ∈ nhdsWithin x s.

Русский

Если f непрерывно внутри s в x и t ∈ nhds (f x), тогда f⁻¹'(t) ∈ nhdsWithin x s.

LaTeX

$$$ (h : ContinuousWithinAt f s x) \rightarrow (t ∈ 𝓝 (f x)) \rightarrow f^{-1}' t ∈ 𝓝[s] x $$$

Lean4

theorem preimage_mem_nhdsWithin {t : Set β} (h : ContinuousWithinAt f s x) (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝[s] x :=
  h ht

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