α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set β
h : Set.Finite (f ⁻¹' s)
hs : s ⊆ range f
⊢ Set.Finite (f '' (f ⁻¹' s))
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set β
h : Set.Finite (f ⁻¹' s)
hs : s ⊆ range f
⊢ Set.Finite s
rw [← image_preimage_eq_of_subset hs]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set β
h : Set.Finite (f ⁻¹' s)
hs : s ⊆ range f
⊢ Set.Finite (f '' (f ⁻¹' s))
exact Finite.image f h