continuousWithinAt_iff_continuousAt

English

If f and g are equal on s, then ContinuousOn f s iff ContinuousOn g s.

Русский

Если функции f и g равны на s, то ContinuousOn f s эквивалентно ContinuousOn g s.

LaTeX

$$$$\text{EqOn}(g,f,s) \Rightarrow (\text{ContinuousOn}(g,s) \iff \text{ContinuousOn}(f,s)).$$$$

Lean4

theorem continuousWithinAt_iff_continuousAt (h : s ∈ 𝓝 x) : ContinuousWithinAt f s x ↔ ContinuousAt f x := by
  rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]

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