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.

source
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
Instances For
    source
    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
    Instances For
      source
      @[simp]
      theorem Set.mem_op {α : Type u_1} {s : Set α} {a : αᵒᵖ} :
      a ∈ s.op ↔ a.unop ∈ s
      source
      @[simp]
      theorem Set.op_mem_op {α : Type u_1} {s : Set α} {a : α} :
      { unop := a } ∈ s.op ↔ a ∈ s
      source
      @[simp]
      theorem Set.mem_unop {α : Type u_1} {s : Set αᵒᵖ} {a : α} :
      a ∈ s.unop ↔ { unop := a } ∈ s
      source
      @[simp]
      theorem Set.unop_mem_unop {α : Type u_1} {s : Set αᵒᵖ} {a : αᵒᵖ} :
      a.unop ∈ 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.opEquiv_self_symm_apply_coe {α : Type u_1} (s : Set α) (x : ↑s) :
      ↑(s.opEquiv_self.symm x) = { unop := ↑x }
      source
      @[simp]
      theorem Set.opEquiv_self_apply_coe {α : Type u_1} (s : Set α) (x : ↑s.op) :
      ↑(s.opEquiv_self x) = (↑x).unop
      source
      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) => ⟨(↑x).unop, ⋯⟩, invFun := fun (x : ↑s) => ⟨{ unop := ↑x }, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
      Instances For
        source
        @[simp]
        theorem Set.opEquiv_apply {α : Type u_1} (s : Set α) :
        Set.opEquiv s = s.op
        source
        @[simp]
        theorem Set.opEquiv_symm_apply {α : Type u_1} (s : Set αᵒᵖ) :
        Set.opEquiv.symm s = s.unop
        source
        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 := ⋯ }
        Instances For
          source
          @[simp]
          theorem Set.singleton_op {α : Type u_1} (x : α) :
          {x}.op = {{ unop := x }}
          source
          @[simp]
          theorem Set.singleton_unop {α : Type u_1} (x : αᵒᵖ) :
          {x}.unop = {x.unop}
          source
          @[simp]
          theorem Set.singleton_op_unop {α : Type u_1} (x : α) :
          {{ unop := x }}.unop = {x}
          source
          @[simp]
          theorem Set.singleton_unop_op {α : Type u_1} (x : αᵒᵖ) :
          {x.unop}.op = {x}