Documentation

Mathlib.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.

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

Set.op s = 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

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

@[simp]

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

a ∈ Set.op s ↔ Opposite.unop a ∈ s

@[simp]

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

Opposite.op a ∈ Set.op s ↔ a ∈ s

@[simp]

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

a ∈ Set.unop s ↔ Opposite.op a ∈ s

@[simp]

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

Opposite.unop a ∈ Set.unop s ↔ a ∈ s

@[simp]

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

Set.unop (Set.op s) = s

@[simp]

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

Set.op (Set.unop s) = s

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

def Set.opEquiv_self {α : Type u_1} (s : Set α) :

↑(Set.op s) ≃ ↑s

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

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

↑Set.opEquiv s = Set.op s

@[simp]

theorem Set.opEquiv_symm_apply {α : Type u_1} (s : Set αᵒᵖ) :

↑(Equiv.symm Set.opEquiv) s = Set.unop s

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 := (_ : ∀ (s : Set α), Set.unop (Set.op s) = s), right_inv := (_ : ∀ (s : Set αᵒᵖ), Set.op (Set.unop s) = s) }

@[simp]

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

Set.op {x} = {Opposite.op x}

@[simp]

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

Set.unop {x} = {Opposite.unop x}

@[simp]

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

Set.unop {Opposite.op x} = {x}

@[simp]

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

Set.op {Opposite.unop x} = {x}