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 open left side Iio(a) and the open right side Ioi(a) are continuous at a.
Русский
Пусть α — линейно упорядоченное топологическое пространство и β — топологическое пространство. Для произвольного a ∈ α и функции f: α → β, функция непрерывна в a тогда и только тогда, когда ее ограничения к открытым левой стороне Iio(a) и правой стороне Ioi(a) непрерывны в a.
LaTeX
$$$\operatorname{ContinuousAt}(f,a) \Longleftrightarrow \operatorname{ContinuousWithinAt}(f,\mathrm{Iio}(a),a) \land \operatorname{ContinuousWithinAt}(f,\mathrm{Ioi}(a),a)$$$
Lean4
theorem continuousAt_iff_continuous_left'_right' {a : α} {f : α → β} :
ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a := by
rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic, continuousAt_iff_continuous_left_right]
