English
ContinuousOn f s holds if and only if for every x in s and every open set t in β containing f(x), there exists an open neighborhood u of x with u ∩ s ⊆ f^{-1}(t).
Русский
Функция f непрерывна на s тогда и только тогда, когда для каждого x ∈ s и каждой открытой множественности t в β с f(x) ∈ t существует открытое окрестность u x, такое что u ∩ s ⊆ f^{-1}(t).
LaTeX
$$$\\text{ContinuousOn } f\\ s \\iff \\forall x\\in s, \\forall t\\subseteq \\beta,\\ IsOpen\\ t \\to f(x)\\in t \\to \\exists u,\\ IsOpen\\ u \\land x\\in u \\land u \\cap s \\subseteq f^{-1}(t)$$$
Lean4
theorem continuousOn_iff :
ContinuousOn f s ↔ ∀ x ∈ s, ∀ t : Set β, IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t := by
simp only [ContinuousOn, ContinuousWithinAt, tendsto_nhds, mem_nhdsWithin]
