nhdsWithin_le_comap — Mathlib

English

For a continuous within f on s at x, the nhdsWithin x s is less than or equal to the comap of f to the nhds within f x of image f s.

Русский

Для непрерывности внутри f на s в x, nhdsWithin x s не превышает обобщение через f к nhdsWithin (f x) образа f s.

LaTeX

$$$ (ctsf : ContinuousWithinAt f s x) \\Rightarrow 𝓝[s] x \\le\\ wedge\\ comap f (\\mathcal{N} [(image f s)] (f x)) $$$$

Lean4

theorem nhdsWithin_le_comap (ctsf : ContinuousWithinAt f s x) : 𝓝[s] x ≤ comap f (𝓝[f '' s] f x) :=
  ctsf.tendsto_nhdsWithin_image.le_comap

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