The opposite of a set #

The opposite of a set s is simply the set obtained by taking the opposite of each member of s.

def Set.op {α : Type u_1} (s : Set α) :

The opposite of a set s is the set obtained by taking the opposite of each member of s.

Equations
Instances For
def Set.unop {α : Type u_1} (s : ) :
Set α

The unop of a set s is the set obtained by taking the unop of each member of s.

Equations
Instances For
@[simp]
theorem Set.mem_op {α : Type u_1} {s : Set α} {a : αᵒᵖ} :
a s.op a.unop s
@[simp]
theorem Set.op_mem_op {α : Type u_1} {s : Set α} {a : α} :
{ unop := a } s.op a s
@[simp]
theorem Set.mem_unop {α : Type u_1} {s : } {a : α} :
a s.unop { unop := a } s
@[simp]
theorem Set.unop_mem_unop {α : Type u_1} {s : } {a : αᵒᵖ} :
a.unop s.unop a s
@[simp]
theorem Set.op_unop {α : Type u_1} (s : Set α) :
s.op.unop = s
@[simp]
theorem Set.unop_op {α : Type u_1} (s : ) :
s.unop.op = s
@[simp]
theorem Set.opEquiv_self_symm_apply_coe {α : Type u_1} (s : Set α) (x : s) :
(s.opEquiv_self.symm x) = { unop := x }
@[simp]
theorem Set.opEquiv_self_apply_coe {α : Type u_1} (s : Set α) (x : s.op) :
(s.opEquiv_self x) = (x).unop
def Set.opEquiv_self {α : Type u_1} (s : Set α) :
s.op s

The members of the opposite of a set are in bijection with the members of the set itself.

Equations
• s.opEquiv_self = { toFun := fun (x : s.op) => (x).unop, , invFun := fun (x : s) => { unop := x }, , left_inv := , right_inv := }
Instances For
@[simp]
theorem Set.opEquiv_apply {α : Type u_1} (s : Set α) :
Set.opEquiv s = s.op
@[simp]
theorem Set.opEquiv_symm_apply {α : Type u_1} (s : ) :
Set.opEquiv.symm s = s.unop
def Set.opEquiv {α : Type u_1} :
Set α

Taking opposites as an equivalence of powersets.

Equations
• Set.opEquiv = { toFun := Set.op, invFun := Set.unop, left_inv := , right_inv := }
Instances For
@[simp]
theorem Set.singleton_op {α : Type u_1} (x : α) :
{x}.op = {{ unop := x }}
@[simp]
theorem Set.singleton_unop {α : Type u_1} (x : αᵒᵖ) :
{x}.unop = {x.unop}
@[simp]
theorem Set.singleton_op_unop {α : Type u_1} (x : α) :
{{ unop := x }}.unop = {x}
@[simp]
theorem Set.singleton_unop_op {α : Type u_1} (x : αᵒᵖ) :
{x.unop}.op = {x}