class Cons (β : outParam (Type u_1)) (α : Type u_2) : Type (max u_1 u_2)

• cons : β → α → α

instance instConsSet (α : Type u_1) : Cons α (Set α)

Equations

• instConsSet α = { cons := insert }

instance instConsList (α : Type u_1) : Cons α (List α)

Equations

• instConsList α = { cons := List.cons }

instance instConsMultiset (α : Type u_1) : Cons α (Multiset α)

Equations

• instConsMultiset α = { cons := Multiset.cons }

instance instConsFinsetOfDecidableEq (α : Type u_1) [DecidableEq α] : Cons α (Finset α)

Equations

• instConsFinsetOfDecidableEq α = { cons := insert }

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 ↔ ∀ x ∈ a, x ∈ b
• not_mem_empty (x : β) : x ∉ ∅
• mem_cons_iff {x z : β} {a : α} : x ∈ cons z a ↔ x = z ∨ x ∈ a

instance Set.collection {α : Type u_1} : Collection α (Set α)

Equations

• Set.collection = Collection.mk ⋯ ⋯ ⋯

instance List.collection {α : Type u_1} : Collection α (List α)

Equations

• List.collection = Collection.mk ⋯ ⋯ ⋯

instance Multiset.collection {α : Type u_1} : Collection α (Multiset α)

Equations

• Multiset.collection = Collection.mk ⋯ ⋯ ⋯

instance Finset.collection {α : Type u_1} [DecidableEq α] : Collection α (Finset α)

Equations

• Finset.collection = Collection.mk ⋯ ⋯ ⋯

def Collection.set {β : Type u_1} {α : Type u_2} [Collection β α] : α → Set β

Equations

• Collection.set a = {x : β | x ∈ a}

@[simp]

theorem Collection.mem_set_iff {β : Type u_1} {α : Type u_2} [Collection β α] {x : β} {a : α} : x ∈ set a ↔ x ∈ a

theorem Collection.subset_iff_set_subset_set {β : Type u_1} {α : Type u_2} [Collection β α] {a b : α} : a ⊆ b ↔ set a ⊆ set 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) : set a = set b

@[simp]

theorem Collection.empty_subset {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) : ∅ ⊆ 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 β α] : set ∅ = ∅

@[simp]

theorem Collection.set_cons {β : Type u_1} {α : Type u_2} [Collection β α] (z : β) (a : α) : set (cons z a) = insert z (set a)

def Collection.Finite {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) : Prop

Equations

• Collection.Finite a = (Collection.set a).Finite

@[simp]

theorem Collection.empty_finite {β : Type u_1} {α : Type u_2} [Collection β α] : Finite ∅

theorem Collection.Finite.of_subset {β : Type u_1} {α : Type u_2} [Collection β α] {a b : α} (ha : Finite a) (h : b ⊆ a) : Finite b

@[simp]

theorem Collection.cons_finite_iff {β : Type u_1} {α : Type u_2} [Collection β α] {z : β} {a : α} : Finite (cons z a) ↔ Finite a

def Collection.addList {β : Type u_1} {α : Type u_2} [Collection β α] (a : α) : List β → α

Equations

• Collection.addList a [] = a
• Collection.addList a (x_1 :: xs) = cons x_1 (Collection.addList a xs)

def List.toCollection {β : Type u_1} {α : Type u_2} [Collection β α] : List β → α

Equations

• [].toCollection = ∅
• (x_1 :: xs).toCollection = cons x_1 xs.toCollection

noncomputable def Finset.toCollection {β : Type u_1} {α : Type u_2} [Collection β α] : Finset β → α

Equations

• s.toCollection = s.toList.toCollection

@[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 β) : Finite l.toCollection

@[simp]

theorem Collection.finset_toCollection_finite {β : Type u_1} {α : Type u_2} [Collection β α] (s : Finset β) : 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 α) : Collection.set s = s

@[simp]

theorem Set.collection_finite_iff {α : Type u_1} (s : Set α) : Collection.Finite s ↔ s.Finite