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

              Taking opposites as an equivalence of powersets.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem Set.opEquiv_apply {α : Type u_1} (s : Set α) :
                  opEquiv s = s.op
                  source
                  @[simp]
                  theorem Set.opEquiv_symm_apply {α : Type u_1} (s : Set αᵒᵖ) :
                  opEquiv.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}