theorem Set.image_neg_of_apply_neg_eq {α : Type u_1} {β : Type u_2} [InvolutiveNeg α] {s : Set α} {f g : α → β} (H : ∀ x ∈ s, f (-x) = g x) : f '' (-s) = g '' s

theorem Set.image_neg_of_apply_neg_eq_neg {α : Type u_1} {β : Type u_2} [InvolutiveNeg α] [InvolutiveNeg β] {s : Set α} {f g : α → β} (H : ∀ x ∈ s, f (-x) = -g x) : f '' (-s) = -g '' s