continuousWithinAt_iff_continuousAt_restrict

English

Let f: α → β and a ∈ s. Then f is continuous within s at a if and only if the restricted function s.restrict f is continuous at ⟨a, h⟩.

Русский

Пусть f: α → β и a ∈ s. Тогда f непрерывна внутри s в точке a тогда и только тогда ограничение f на s непрерывно в точке ⟨a⟩.

LaTeX

$$$ (h : a ∈ s) \\Rightarrow (ContinuousWithinAt f s a \\iff ContinuousAt (s.restrict f) (\\langle a, h \\rangle)) $$$

Lean4

theorem continuousWithinAt_iff_continuousAt_restrict (f : α → β) {x : α} {s : Set α} (h : x ∈ s) :
    ContinuousWithinAt f s x ↔ ContinuousAt (s.restrict f) ⟨x, h⟩ :=
  tendsto_nhdsWithin_iff_subtype h f _

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