continuousWithinAt_iff_continuous_left_right

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]

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