@[simp]

theorem Set.neg_setOf {α : Type u_1} [InvolutiveNeg α] (p : α → Prop) : -{x : α | p x} = {x : α | p (-x)}

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

instance Set.instSmallElemNeg_combinatorialGames {α : Type u_1} [InvolutiveNeg α] (s : Set α) [Small.{u, u_1} ↑s] : Small.{u, u_1} ↑(-s)

@[simp]

theorem Set.forall_mem_neg {α : Type u_1} [InvolutiveNeg α] {p : α → Prop} {s : Set α} : (∀ (x : α), -x ∈ s → p x) ↔ ∀ x ∈ s, p (-x)

@[simp]

theorem Set.exists_mem_neg {α : Type u_1} [InvolutiveNeg α] {p : α → Prop} {s : Set α} : (∃ (x : α), -x ∈ s ∧ p x) ↔ ∃ x ∈ s, p (-x)