continuousWithinAt_iff_continuous_left'_right'

English

For any a ∈ α and f : α → β, ContinuousWithinAt f s a is equivalent to the conjunction of the continuities on s ∩ Iio(a) and s ∩ Ioi(a).

Русский

Для произвольного a ∈ α и функции f: α → β, непрерывность внутри s в a эквивалентна непрерывности на s ∩ Iio(a) и на s ∩ Ioi(a).

LaTeX

$$$\operatorname{ContinuousWithinAt}(f,s,a) \iff \operatorname{ContinuousWithinAt}(f, s \cap \mathrm{Iio}(a), a) \land \operatorname{ContinuousWithinAt}(f, s \cap \mathrm{Ioi}(a), a)$$$

Lean4

theorem continuousWithinAt_iff_continuous_left'_right' {a : α} {f : α → β} :
    ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ioi a) a := by
  rw [continuousWithinAt_inter_Ioi_iff_Ici, continuousWithinAt_inter_Iio_iff_Iic,
    continuousWithinAt_iff_continuous_left_right]

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