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 α) : Set αᵒᵖ

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

Equations

• s.op = Opposite.unop ⁻¹' s

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

• s.unop = Opposite.op ⁻¹' s

@[simp]

theorem Set.mem_op {α : Type u_1} {s : Set α} {a : αᵒᵖ} : a ∈ s.op ↔ Opposite.unop a ∈ s

@[simp]

theorem Set.op_mem_op {α : Type u_1} {s : Set α} {a : α} : Opposite.op a ∈ s.op ↔ a ∈ s

@[simp]

theorem Set.mem_unop {α : Type u_1} {s : Set αᵒᵖ} {a : α} : a ∈ s.unop ↔ Opposite.op a ∈ s

@[simp]

theorem Set.unop_mem_unop {α : Type u_1} {s : Set αᵒᵖ} {a : αᵒᵖ} : Opposite.unop a ∈ 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 : Set αᵒᵖ) : s.unop.op = s

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) => ⟨Opposite.unop ↑x, ⋯⟩, invFun := fun (x : ↑s) => ⟨Opposite.op ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Set.opEquiv_self_symm_apply_coe {α : Type u_1} (s : Set α) (x : ↑s) : ↑(s.opEquiv_self.symm x) = Opposite.op ↑x

@[simp]

theorem Set.opEquiv_self_apply_coe {α : Type u_1} (s : Set α) (x : ↑s.op) : ↑(s.opEquiv_self x) = Opposite.unop ↑x

def Set.opEquiv {α : Type u_1} : Set α ≃ Set αᵒᵖ

Taking opposites as an equivalence of powersets.

Equations

• Set.opEquiv = { toFun := Set.op, invFun := Set.unop, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Set.opEquiv_apply {α : Type u_1} (s : Set α) : opEquiv s = s.op

@[simp]

theorem Set.opEquiv_symm_apply {α : Type u_1} (s : Set αᵒᵖ) : opEquiv.symm s = s.unop

@[simp]

theorem Set.singleton_op {α : Type u_1} (x : α) : {x}.op = {Opposite.op x}

@[simp]

theorem Set.singleton_unop {α : Type u_1} (x : αᵒᵖ) : {x}.unop = {Opposite.unop x}

@[simp]

theorem Set.singleton_op_unop {α : Type u_1} (x : α) : {Opposite.op x}.unop = {x}

@[simp]

theorem Set.singleton_unop_op {α : Type u_1} (x : αᵒᵖ) : {Opposite.unop x}.op = {x}