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]
theorem
Set.opEquiv_self_symm_apply_coe
{α : Type u_1}
(s : Set α)
(x : ↑s)
:
↑(↑(Equiv.symm (Set.opEquiv_self s)) x) = Opposite.op ↑x
@[simp]
theorem
Set.opEquiv_self_apply_coe
{α : Type u_1}
(s : Set α)
(x : ↑(Set.op s))
:
↑(↑(Set.opEquiv_self s) x) = Opposite.unop ↑x
@[simp]
theorem
Set.opEquiv_symm_apply
{α : Type u_1}
(s : Set αᵒᵖ)
:
↑(Equiv.symm Set.opEquiv) s = Set.unop s
@[simp]
@[simp]
@[simp]