continuousOn_of_locally_continuousOn

English

If for every x ∈ s there exists an open neighborhood t with x ∈ t and ContinuousOn f (s ∩ t), then f is ContinuousOn on s.

Русский

Если для каждого x ∈ s существует открытое окружение t с x ∈ t и ContinuousOn f (s ∩ t), то f непрерывна на s.

LaTeX

$$$\\forall x \\in s, \\exists t\\text{ open}, x \\in t \\land ContinuousOn f (s \\cap t) \\Rightarrow ContinuousOn f s$$$

Lean4

theorem continuousOn_of_locally_continuousOn (h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)) :
    ContinuousOn f s := by
  intro x xs
  rcases h x xs with ⟨t, open_t, xt, ct⟩
  have := ct x ⟨xs, xt⟩
  rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this

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