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
.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
set.op_equiv_self_apply_coe
{α : Type u_1}
(s : set α)
(x : ↥(s.op)) :
↑(⇑(s.op_equiv_self) x) = opposite.unop ↑x
@[simp]
theorem
set.op_equiv_self_symm_apply_coe
{α : Type u_1}
(s : set α)
(x : ↥s) :
↑(⇑(s.op_equiv_self.symm) x) = opposite.op ↑x
The members of the opposite of a set are in bijection with the members of the set itself.
@[simp]