The opposite of a set #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

@[protected]

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

source

@[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

s.unop = opposite.op ⁻¹' s

source

@[simp]

theorem set.mem_op {α : Type u_1} {s : set α} {a : αᵒᵖ} :

a ∈ s.op ↔ opposite.unop a ∈ s

source

@[simp]

theorem set.op_mem_op {α : Type u_1} {s : set α} {a : α} :

opposite.op a ∈ s.op ↔ a ∈ s

source

@[simp]

theorem set.mem_unop {α : Type u_1} {s : set αᵒᵖ} {a : α} :

a ∈ s.unop ↔ opposite.op a ∈ s

source

@[simp]

theorem set.unop_mem_unop {α : Type u_1} {s : set αᵒᵖ} {a : αᵒᵖ} :

opposite.unop a ∈ s.unop ↔ a ∈ s

source

@[simp]

theorem set.op_unop {α : Type u_1} (s : set α) :

s.op.unop = s

source

@[simp]

theorem set.unop_op {α : Type u_1} (s : set αᵒᵖ) :

s.unop.op = s

source

@[simp]

theorem set.op_equiv_self_apply_coe {α : Type u_1} (s : set α) (x : ↥(s.op)) :

↑(⇑(s.op_equiv_self) x) = opposite.unop ↑x

source

@[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

source

def set.op_equiv_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.op_equiv_self = {to_fun := λ (x : ↥(s.op)), ⟨opposite.unop ↑x, _⟩, inv_fun := λ (x : ↥s), ⟨opposite.op ↑x, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem set.op_equiv_apply {α : Type u_1} (s : set α) :

⇑set.op_equiv s = s.op

source

def set.op_equiv {α : Type u_1} :

set α ≃ set αᵒᵖ

Taking opposites as an equivalence of powersets.

Equations

set.op_equiv = {to_fun := set.op α, inv_fun := set.unop α, left_inv := _, right_inv := _}

source

@[simp]

theorem set.op_equiv_symm_apply {α : Type u_1} (s : set αᵒᵖ) :

⇑(set.op_equiv.symm) s = s.unop

source

@[simp]

theorem set.singleton_op {α : Type u_1} (x : α) :

{x}.op = {opposite.op x}

source

@[simp]

theorem set.singleton_unop {α : Type u_1} (x : αᵒᵖ) :

{x}.unop = {opposite.unop x}

source

@[simp]

theorem set.singleton_op_unop {α : Type u_1} (x : α) :

{opposite.op x}.unop = {x}

source

@[simp]

theorem set.singleton_unop_op {α : Type u_1} (x : αᵒᵖ) :

{opposite.unop x}.op = {x}