Documentation

Std.Classes.SetNotation

class HasSubset (α : Type u) :
  • Subset relation: a ⊆ b⊆ b

    Subset : ααProp

Notation type class for the subset relation ⊆⊆.

Instances
    class HasSSubset (α : Type u) :
    • Strict subset relation: a ⊂ b⊂ b

      SSubset : ααProp

    Notation type class for the strict subset relation ⊂⊂.

    Instances

      Strict subset relation: a ⊂ b⊂ b

      Equations
      @[inline]
      abbrev Superset {α : Type u_1} [inst : HasSubset α] (a : α) (b : α) :

      Superset relation: a ⊇ b⊇ b

      Equations
      @[inline]
      abbrev SSuperset {α : Type u_1} [inst : HasSSubset α] (a : α) (b : α) :

      Strict superset relation: a ⊃ b⊃ b

      Equations

      Strict superset relation: a ⊃ b⊃ b

      Equations
      class Union (α : Type u) :
      • a ∪ b∪ b is the union ofa and b.

        union : ααα

      Notation type class for the union operation ∪∪.

      Instances

        a ∪ b∪ b is the union ofa and b.

        Equations
        class Inter (α : Type u) :
        • a ∩ b∩ b is the intersection ofa and b.

          inter : ααα

        Notation type class for the intersection operation ∩∩.

        Instances

          a ∩ b∩ b is the intersection ofa and b.

          Equations
          class SDiff (α : Type u) :
          • a \ b is the set difference of a and b, consisting of all elements in a that are not in b.

            sdiff : ααα

          Notation type class for the set difference \.

          Instances

            a \ b is the set difference of a and b, consisting of all elements in a that are not in b.

            Equations
            class Insert (α : outParam (Type u)) (γ : Type v) :
            Type (maxuv)
            • insert x xs inserts the element x into the collection xs.

              insert : αγγ

            Type class for the insert operation. Used to implement the { a, b, c } syntax.

            Instances
              class Singleton (α : outParam (Type u)) (β : Type v) :
              Type (maxuv)
              • singleton x is a collection with the single element x (notation: {x}).

                singleton : αβ

              Type class for the singleton operation. Used to implement the { a, b, c } syntax.

              Instances
                class Sep (α : outParam (Type u)) (γ : Type v) :
                Type (maxuv)
                • Computes { a ∈ c | p a }∈ c | p a }.

                  sep : (αProp) → γγ

                Type class used to implement the notation { a ∈ c | p a }∈ c | p a }

                Instances

                  Declare ∃ x ∈ y, ...∃ x ∈ y, ...∈ y, ... as syntax for ∃ x, x ∈ y ∧ ...∃ x, x ∈ y ∧ ...∈ y ∧ ...∧ ...

                  Equations

                  { a, b, c } is a set with elements a, b, and c.

                  This notation works for all types that implement Insert and Singleton.

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

                  Unexpander for the { x } notation.

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

                  Unexpander for the { x, y, ... } notation.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  class IsLawfulSingleton (α : Type u) (β : Type v) [inst : EmptyCollection β] [inst : Insert α β] [inst : Singleton α β] :
                  • insert x ∅ = {x}∅ = {x}

                    insert_emptyc_eq : ∀ (x : α), insert x = {x}

                  insert x ∅ = {x}∅ = {x}

                  Instances