α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}
classical rw [← Fintype.coe_image_univ, univ_eq]
no goals
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
classical simp [Finset.coe_insert]
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}
rw [← Fintype.coe_image_univ, univ_eq]
no goals
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
simp [Finset.coe_insert]