α : Type u_1
β : Type u_2
γ : Type ?u.380506
δ : Type ?u.380509
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => if p a then f a else g a) univ
α : Type u_1
β : Type u_2
γ : Type ?u.380506
δ : Type ?u.380509
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ Continuous fun a => if p a then f a else g a
rw [continuous_iff_continuousOn_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.380506
δ : Type ?u.380509
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => if p a then f a else g a) univ
apply ContinuousOn.if <;> simp <;> assumption