α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
⊢ ContinuousOn (fun a => if p a then f a else g a) s
intro x hx
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : ¬x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x
by_cases hx' : x ∈ frontier { a | p a }
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x
exact (hpf x ⟨hx, hx'⟩).piecewise_nhdsWithin (hpg x ⟨hx, hx'⟩)
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ
hx' : ¬x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : ¬x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x
rw [← inter_univ s, ← union_compl_self { a | p a }, inter_union_distrib_left] at hx ⊢
case neg.inl
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x

case neg.inr
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ
hx' : ¬x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
cases' hx with hx hx
case neg.inl.hs
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x

case neg.inl.ht
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
case neg.inl
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
apply ContinuousWithinAt.union
no goals
case neg.inl.hs
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x
exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)
case neg.inl.ht
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
this : ¬x ∈ closure ({a | p a}ᶜ)
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
case neg.inl.ht
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
have : x ∉ closure ({ a | p a }ᶜ) := fun h => hx' ⟨subset_closure hx.2, by
  rwa [closure_compl] at h⟩
no goals
case neg.inl.ht
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
this : ¬x ∈ closure ({a | p a}ᶜ)
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
exact continuousWithinAt_of_not_mem_closure fun h =>
  this (closure_inter_subset_inter_closure _ _ h).2
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
h : x ∈ closure ({a | p a}ᶜ)
⊢ ¬x ∈ interior {a | p a}
rwa [closure_compl] at h
case neg.inr.hs
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x

case neg.inr.ht
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
case neg.inr
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
apply ContinuousWithinAt.union
case neg.inr.hs
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
this : ¬x ∈ closure {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x
case neg.inr.hs
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x
have : x ∉ closure { a | p a } := fun h =>
  hx' ⟨h, fun h' : x ∈ interior { a | p a } => hx.2 (interior_subset h')⟩
no goals
case neg.inr.hs
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
this : ¬x ∈ closure {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x
exact continuousWithinAt_of_not_mem_closure fun h =>
  this (closure_inter_subset_inter_closure _ _ h).2
no goals
case neg.inr.ht
α : Type u_1
β : Type u_2
γ : Type ?u.370900
δ : Type ?u.370903
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)