[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
simp only [← Ici_diff_left, continuousWithinAt_diff_self]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iic a] a ⊔ 𝓝[Ici a] a = 𝓝 a
[PROOFSTEP]
rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iio a] a ⊔ 𝓝[Ici a] a = 𝓝 a
[PROOFSTEP]
rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iic a] a ⊔ 𝓝[Ioi a] a = 𝓝 a
[PROOFSTEP]
rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iio a] a ⊔ 𝓝[Ioi a] a = 𝓝[{a}ᶜ] a
[PROOFSTEP]
rw [← nhdsWithin_union, Iio_union_Ioi]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhds_left_sup_nhds_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a
[PROOFSTEP]
rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic, continuousAt_iff_continuous_left_right]
