English
Let α be a linearly ordered topological space and β a topological space. For any a ∈ α and any f : α → β, f is continuous at a if and only if its restrictions to the left and to the right of a are continuous at a, i.e. the restrictions to (−∞, a] and [a, ∞) are each continuous at a.
Русский
Пусть α — линейно упорядоченное топологическое пространство и β — топологическое пространство. Для произвольного a ∈ α и функции f: α → β, функция непрерывна в точке a тогда и только тогда, когда ее ограничения слева и справа от a непрерывны в точке a, то есть ограничения на (-∞, a] и [a, ∞) непрерывны в a.
LaTeX
$$$\operatorname{ContinuousAt}(f,a) \Longleftrightarrow \operatorname{ContinuousWithinAt}(f,(-\infty,a],a) \land \operatorname{ContinuousWithinAt}(f,[a,\infty),a)$$$
Lean4
theorem continuousAt_iff_continuous_left_right {a : α} {f : α → β} :
ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a := by
simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhdsLE_sup_nhdsGE]
