Documentation

Foundation.Vorspiel.Collection

class Cons (β : outParam (Type u_1)) (α : Type u_2) :
Type (max u_1 u_2)
  • cons : βαα
Instances
    instance instConsSet (α : Type u_1) :
    Cons α (Set α)
    Equations
    instance instConsList (α : Type u_1) :
    Cons α (List α)
    Equations
    instance instConsMultiset (α : Type u_1) :
    Cons α (Multiset α)
    Equations
    instance instConsFinsetOfDecidableEq (α : Type u_1) [DecidableEq α] :
    Cons α (Finset α)
    Equations
    class Collection (β : outParam (Type u_1)) (α : Type u_2) extends Membership , HasSubset , EmptyCollection , Cons :
    Type (max u_1 u_2)
    • mem : βαProp
    • Subset : ααProp
    • emptyCollection : α
    • cons : βαα
    • subset_iff : ∀ {a b : α}, a b xa, x b
    • not_mem_empty : ∀ (x : β), x
    • mem_cons_iff : ∀ {x z : β} {a : α}, x cons z a x = z x a
    Instances
      theorem Collection.subset_iff {β : outParam (Type u_1)} {α : Type u_2} [self : Collection β α] {a : α} {b : α} :
      a b xa, x b
      @[simp]
      theorem Collection.not_mem_empty {β : outParam (Type u_1)} {α : Type u_2} [self : Collection β α] (x : β) :
      x
      @[simp]
      theorem Collection.mem_cons_iff {β : outParam (Type u_1)} {α : Type u_2} [self : Collection β α] {x : β} {z : β} {a : α} :
      x cons z a x = z x a
      instance Set.collection {α : Type u_1} :
      Collection α (Set α)
      Equations
      instance List.collection {α : Type u_1} :
      Equations
      instance Multiset.collection {α : Type u_1} :
      Equations
      instance Finset.collection {α : Type u_1} [DecidableEq α] :
      Equations
      def Collection.set {β : Type u_1} {α : Type u_2} [Collection β α] :
      αSet β
      Equations
      Instances For
        @[simp]
        theorem Collection.mem_set_iff {β : Type u_1} {α : Type u_2} [Collection β α] {x : β} {a : α} :
        theorem Collection.subset_iff_set_subset_set {β : Type u_1} {α : Type u_2} [Collection β α] {a : α} {b : α} :
        @[simp]
        theorem Collection.subset_refl {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) :
        a a
        theorem Collection.subset_trans {β : Type u_1} {α : Type u_2} [Collection β α] {a : α} {b : α} {c : α} (ha : a b) (hb : b c) :
        a c
        theorem Collection.subset_antisymm {β : Type u_1} {α : Type u_2} [Collection β α] {a : α} {b : α} (ha : a b) (hb : b a) :
        @[simp]
        theorem Collection.empty_subset {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) :
        @[simp]
        theorem Collection.mem_cons {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) (x : β) :
        x cons x a
        @[simp]
        theorem Collection.subset_cons {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) (x : β) :
        a cons x a
        @[simp]
        theorem Collection.set_empty {β : Type u_1} {α : Type u_2} [Collection β α] :
        @[simp]
        theorem Collection.set_cons {β : Type u_1} {α : Type u_2} [Collection β α] (z : β) (a : α) :
        def Collection.Finite {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) :
        Equations
        Instances For
          @[simp]
          theorem Collection.empty_finite {β : Type u_1} {α : Type u_2} [Collection β α] :
          theorem Collection.Finite.of_subset {β : Type u_1} {α : Type u_2} [Collection β α] {a : α} {b : α} (ha : Collection.Finite a) (h : b a) :
          @[simp]
          theorem Collection.cons_finite_iff {β : Type u_1} {α : Type u_2} [Collection β α] {z : β} {a : α} :
          def Collection.addList {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) :
          List βα
          Equations
          Instances For
            def List.toCollection {β : Type u_1} {α : Type u_2} [Collection β α] :
            List βα
            Equations
            • [].toCollection =
            • (x_1 :: xs).toCollection = cons x_1 xs.toCollection
            Instances For
              noncomputable def Finset.toCollection {β : Type u_1} {α : Type u_2} [Collection β α] :
              Finset βα
              Equations
              • s.toCollection = s.toList.toCollection
              Instances For
                @[simp]
                theorem Collection.mem_list_toCollection {β : Type u_1} {α : Type u_2} [Collection β α] {x : β} {l : List β} :
                x l.toCollection x l
                @[simp]
                theorem Collection.mem_finset_toCollection {β : Type u_1} {α : Type u_2} [Collection β α] {x : β} {s : Finset β} :
                x s.toCollection x s
                @[simp]
                theorem Collection.list_toCollection_finite {β : Type u_1} {α : Type u_2} [Collection β α] (l : List β) :
                Collection.Finite l.toCollection
                @[simp]
                theorem Collection.finset_toCollection_finite {β : Type u_1} {α : Type u_2} [Collection β α] (s : Finset β) :
                Collection.Finite s.toCollection
                theorem Set.cons_eq {α : Type u_1} (a : α) (s : Set α) :
                cons a s = insert a s
                @[simp]
                theorem Set.collection_set {α : Type u_1} (s : Set α) :
                @[simp]
                theorem Set.collection_finite_iff {α : Type u_1} (s : Set α) :