English
For any a ∈ α and f : α → β, ContinuousWithinAt f s a is equivalent to the conjunction of the continuities of f on s ∩ Iic(a) and s ∩ Ici(a).
Русский
Для произвольного a ∈ α и функции f: α → β, непрерывность внутри множества s в точке a эквивалентна сочетанию непрерывности f на s ∩ Iic(a) и на s ∩ Ici(a).
LaTeX
$$$\operatorname{ContinuousWithinAt}(f,s,a) \iff \operatorname{ContinuousWithinAt}(f, s \cap \mathrm{Iic}(a), a) \land \operatorname{ContinuousWithinAt}(f, s \cap \mathrm{Ici}(a), a)$$$
Lean4
theorem continuousWithinAt_iff_continuous_left_right {a : α} {f : α → β} :
ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a := by
simp only [ContinuousWithinAt, ← tendsto_sup, nhdsWithinLE_sup_nhdsWithinGE]