mono_of_mem_nhdsWithin — Mathlib

English

If h is ContinuousWithinAt f t x and the neighborhood nhdsWithin x s contains t, then f is continuous within s at x.

Русский

Если h непрерывна внутри t и nhdsWithin x s содержит t, то f непрерывна внутри s в точке x.

LaTeX

$$$h : ContinuousWithinAt f t x \\land hs : t \\in 𝓝[x]s \\Rightarrow ContinuousWithinAt f s x$$$

Lean4

theorem mono_of_mem_nhdsWithin (h : ContinuousWithinAt f t x) (hs : t ∈ 𝓝[s] x) : ContinuousWithinAt f s x :=
  h.mono_left (nhdsWithin_le_of_mem hs)

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