α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
⊢ (∀ (b : α), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b) ∧ (x ∈ s → ContinuousWithinAt (update f x y) s x) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
⊢ ContinuousOn (update f x y) s ↔ ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
rw [ContinuousOn, ← and_forall_ne x, and_comm]
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
H : ∀ (b : α), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b
z : α
hz : z ∈ s \ {x}
⊢ ContinuousWithinAt f (s \ {x}) z

case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
H : ContinuousOn f (s \ {x})
z : α
hzx : z ≠ x
hzs : z ∈ s
⊢ ContinuousWithinAt (update f x y) s z

case refine'_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
x✝ : x ∈ s
⊢ ContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y)
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
⊢ (∀ (b : α), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b) ∧ (x ∈ s → ContinuousWithinAt (update f x y) s x) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
refine' and_congr ⟨fun H z hz => _, fun H z hzx hzs => _⟩ (forall_congr' fun _ => _)
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
z : α
hz : z ∈ s \ {x}
H : ContinuousWithinAt (update f x y) s z
⊢ ContinuousWithinAt f (s \ {x}) z
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
H : ∀ (b : α), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b
z : α
hz : z ∈ s \ {x}
⊢ ContinuousWithinAt f (s \ {x}) z
specialize H z hz.2 hz.1
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
z : α
hz : z ∈ s \ {x}
H : ContinuousWithinAt f s z
⊢ ContinuousWithinAt f (s \ {x}) z
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
z : α
hz : z ∈ s \ {x}
H : ContinuousWithinAt (update f x y) s z
⊢ ContinuousWithinAt f (s \ {x}) z
rw [continuousWithinAt_update_of_ne hz.2] at H
no goals
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
z : α
hz : z ∈ s \ {x}
H : ContinuousWithinAt f s z
⊢ ContinuousWithinAt f (s \ {x}) z
exact H.mono (diff_subset _ _)
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
H : ContinuousOn f (s \ {x})
z : α
hzx : z ≠ x
hzs : z ∈ s
⊢ ContinuousWithinAt f s z
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
H : ContinuousOn f (s \ {x})
z : α
hzx : z ≠ x
hzs : z ∈ s
⊢ ContinuousWithinAt (update f x y) s z
rw [continuousWithinAt_update_of_ne hzx]
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
H : ContinuousOn f (s \ {x})
z : α
hzx : z ≠ x
hzs : z ∈ s
⊢ (fun a => a ∈ {x} → False) ∈ 𝓝 z
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
H : ContinuousOn f (s \ {x})
z : α
hzx : z ≠ x
hzs : z ∈ s
⊢ ContinuousWithinAt f s z
refine' (H z ⟨hzs, hzx⟩).mono_of_mem (inter_mem_nhdsWithin _ _)
no goals
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
H : ContinuousOn f (s \ {x})
z : α
hzx : z ≠ x
hzs : z ∈ s
⊢ (fun a => a ∈ {x} → False) ∈ 𝓝 z
exact isOpen_ne.mem_nhds hzx
no goals
case refine'_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T1Space α
inst✝¹ : DecidableEq α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
y : β
x✝ : x ∈ s
⊢ ContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y)
exact continuousWithinAt_update_same