mathlib documentation

data.set.opposite

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.

@[protected]
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
@[protected]
def set.unop {α : Type u_1} (s : set αᵒᵖ) :
set α

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

Equations
@[simp]
theorem set.mem_op {α : Type u_1} {s : set α} {a : αᵒᵖ} :
@[simp]
theorem set.op_mem_op {α : Type u_1} {s : set α} {a : α} :
@[simp]
theorem set.mem_unop {α : Type u_1} {s : set αᵒᵖ} {a : α} :
@[simp]
theorem set.unop_mem_unop {α : Type u_1} {s : set αᵒᵖ} {a : αᵒᵖ} :
@[simp]
theorem set.op_unop {α : Type u_1} (s : set α) :
s.op.unop = s
@[simp]
theorem set.unop_op {α : Type u_1} (s : set αᵒᵖ) :
s.unop.op = s
@[simp]
theorem set.op_equiv_self_apply_coe {α : Type u_1} (s : set α) (x : (s.op)) :
@[simp]
theorem set.op_equiv_self_symm_apply_coe {α : Type u_1} (s : set α) (x : s) :
def set.op_equiv_self {α : Type u_1} (s : set α) :

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

Equations
@[simp]
theorem set.op_equiv_apply {α : Type u_1} (s : set α) :
def set.op_equiv {α : Type u_1} :

Taking opposites as an equivalence of powersets.

Equations
@[simp]
theorem set.op_equiv_symm_apply {α : Type u_1} (s : set αᵒᵖ) :
@[simp]
theorem set.singleton_op {α : Type u_1} (x : α) :
{x}.op = {opposite.op x}
@[simp]
theorem set.singleton_unop {α : Type u_1} (x : αᵒᵖ) :
@[simp]
theorem set.singleton_op_unop {α : Type u_1} (x : α) :
@[simp]
theorem set.singleton_unop_op {α : Type u_1} (x : αᵒᵖ) :