comp_of_preimage_mem_nhdsWithin — Mathlib

English

If f and g are equal on a neighborhood of x inside s and x ∈ s, then continuity of f on s at x implies continuity of g on s at x.

Русский

Если f и g совпадают на окрестности x внутри s и x ∈ s, то непрерывность f на s в x влечет непрерывность g на s в x.

LaTeX

$$$ (\forall y\in s, g(y)=f(y)) \land x\in s \Rightarrow (ContinuousWithinAt g s x \iff ContinuousWithinAt f s x).$$$

Lean4

theorem comp_of_preimage_mem_nhdsWithin {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x))
    (hf : ContinuousWithinAt f s x) (h : f ⁻¹' t ∈ 𝓝[s] x) : ContinuousWithinAt (g ∘ f) s x :=
  hg.tendsto.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f hf h)

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