continuousOn_of_forall_continuousAt

English

If s ∈ 𝓝 x, then ContinuousWithinAt f s x ↔ ContinuousAt f x.

Русский

Если s принадлежит 𝓝 x, тогда ContinuousWithinAt f s x эквивално ContinuousAt f x.

LaTeX

$$$$s \in 𝓝 x \Rightarrow \bigl(\text{ContinuousWithinAt}(f,s,x) \iff \text{ContinuousAt}(f,x)\bigr).$$$$

Lean4

theorem continuousOn_of_forall_continuousAt (hcont : ∀ x ∈ s, ContinuousAt f x) : ContinuousOn f s := fun x hx =>
  (hcont x hx).continuousWithinAt

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