continuousWithinAt_inter_Ioi_iff_Ici

English

Continuity on s ∩ Ioi a is equivalent to continuity on s ∩ Ici a.

Русский

Непрерывность на s ∩ Ioi a эквивалентна непрерывности на s ∩ Ici a.

LaTeX

$$theorem continuousWithinAt_inter_Ioi_iff_Ici {a : α} {f : α → β} {s : Set α} : ContinuousWithinAt f (s ∩ Ioi a) a ↔ ContinuousWithinAt f (s ∩ Ici a) a$$

Lean4

theorem continuousWithinAt_inter_Ioi_iff_Ici {a : α} {f : α → β} {s : Set α} :
    ContinuousWithinAt f (s ∩ Ioi a) a ↔ ContinuousWithinAt f (s ∩ Ici a) a := by
  simp [← Ici_diff_left, ← inter_diff_assoc, continuousWithinAt_diff_self]

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