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

• cons : β → α → α

Instances

• LO.Arith.instCons_arithmetization
• LO.System.Context.instCons
• LO.System.FiniteContext.instCons
• instConsFinsetOfDecidableEq
• instConsList
• instConsMultiset
• instConsSet

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

Instances

• Finset.collection
• LO.FirstOrder.instCollectionSentenceClosedTheory
• LO.FirstOrder.instCollectionSyntacticFormulaTheory
• LO.Modal.instCollectionFormulaTheory
• LO.Propositional.Classical.instCollectionFormulaTheory
• LO.System.Context.instCollection
• LO.System.FiniteContext.instCollection
• List.collection
• Multiset.collection
• Set.collection

theorem Collection.subset_iff {β : outParam (Type u_1)} {α : Type u_2} [self : Collection β α] {a : α} {b : α} : a ⊆ b ↔ ∀ x ∈ a, 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

• 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 ∈ Collection.set a ↔ x ∈ a

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

@[simp]

theorem Collection.set_cons {β : Type u_1} {α : Type u_2} [Collection β α] (z : β) (a : α) : Collection.set (cons z a) = insert z (Collection.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 β α] : Collection.Finite ∅

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

@[simp]

theorem Collection.cons_finite_iff {β : Type u_1} {α : Type u_2} [Collection β α] {z : β} {a : α} : Collection.Finite (cons z a) ↔ Collection.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 β) : 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 α) : Collection.set s = s

@[simp]

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