continuousOn_iff_continuous_restrict

English

ContinuousOn f s is equivalent to the continuity of the restricted map s.restrict f.

Русский

ContinuousOn f s эквивалентна непрерывности ограниченной карты s.restrict f.

LaTeX

$$$\\text{ContinuousOn } f s \\iff \\text{Continuous }(s\\restriction f)$$$

Lean4

theorem continuousOn_iff_continuous_restrict : ContinuousOn f s ↔ Continuous (s.restrict f) :=
  by
  rw [ContinuousOn, continuous_iff_continuousAt]; constructor
  · rintro h ⟨x, xs⟩
    exact (continuousWithinAt_iff_continuousAt_restrict f xs).mp (h x xs)
  intro h x xs
  exact (continuousWithinAt_iff_continuousAt_restrict f xs).mpr (h ⟨x, xs⟩)

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