preimage_mem_nhdsWithin' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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