α : Type u_1
β : Type u_2
γ : Type ?u.46973
ι : Sort ?u.46976
ι' : Sort ?u.46979
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
H : Surjective f
⊢ f '' (s ∪ sᶜ) = univ
α : Type u_1
β : Type u_2
γ : Type ?u.46973
ι : Sort ?u.46976
ι' : Sort ?u.46979
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
H : Surjective f
⊢ f '' s ∪ f '' sᶜ = univ
rw [← image_union]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.46973
ι : Sort ?u.46976
ι' : Sort ?u.46979
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
H : Surjective f
⊢ f '' (s ∪ sᶜ) = univ
simp [image_univ_of_surjective H]