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

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

instance Set.collection {α : Type u_1} :

Collection α (Set α)

Equations

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

instance List.collection {α : Type u_1} :

Collection α (List α)

Equations

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

instance Multiset.collection {α : Type u_1} :

Collection α (Multiset α)

Equations

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

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

Collection α (Finset α)

Equations

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

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) :

@[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 : α) :

set (cons z a) = insert z (set a)

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

Equations

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

@[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 : Finite a) (h : b ⊆ a) :

@[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