case inl
α : Type u_1
β : Type u_2
γ : Type ?u.383429
δ : Type ?u.383432
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : Prop
f g : α → β
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : p
⊢ Continuous fun a => f a

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.383429
δ : Type ?u.383432
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : Prop
f g : α → β
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : ¬p
⊢ Continuous fun a => g a
α : Type u_1
β : Type u_2
γ : Type ?u.383429
δ : Type ?u.383432
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : Prop
f g : α → β
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
⊢ Continuous fun a => if p then f a else g a
split_ifs with h
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.383429
δ : Type ?u.383432
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : Prop
f g : α → β
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : p
⊢ Continuous fun a => f a

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.383429
δ : Type ?u.383432
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : Prop
f g : α → β
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : ¬p
⊢ Continuous fun a => g a
exacts [hf h, hg h]