Equations
- instConsSet α = { cons := insert }
Equations
- instConsList α = { cons := List.cons }
Equations
- instConsMultiset α = { cons := Multiset.cons }
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 : β → α → α
- not_mem_empty : ∀ (x : β), x ∉ ∅
Instances
theorem
Collection.subset_iff
{β : outParam (Type u_1)}
{α : Type u_2}
[self : Collection β α]
{a : α}
{b : α}
:
@[simp]
theorem
Collection.not_mem_empty
{β : outParam (Type u_1)}
{α : Type u_2}
[self : Collection β α]
(x : β)
:
x ∉ ∅
Equations
- Set.collection = Collection.mk ⋯ ⋯ ⋯
Equations
- List.collection = Collection.mk ⋯ ⋯ ⋯
Equations
- Multiset.collection = Collection.mk ⋯ ⋯ ⋯
Equations
- Finset.collection = Collection.mk ⋯ ⋯ ⋯
Equations
- Collection.set a = {x : β | x ∈ a}
Instances For
@[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_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]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Collection.set_cons
{β : Type u_1}
{α : Type u_2}
[Collection β α]
(z : β)
(a : α)
:
Collection.set (cons z a) = insert z (Collection.set a)
Equations
- Collection.Finite a = (Collection.set a).Finite
Instances For
@[simp]
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 : α}
:
Collection.Finite (cons z a) ↔ Collection.Finite a
Equations
- Collection.addList a [] = a
- Collection.addList a (x_1 :: xs) = cons x_1 (Collection.addList a xs)
Instances For
Equations
- s.toCollection = s.toList.toCollection
Instances For
@[simp]
theorem
Collection.mem_list_toCollection
{β : Type u_1}
{α : Type u_2}
[Collection β α]
{x : β}
{l : List β}
:
@[simp]
theorem
Collection.mem_finset_toCollection
{β : Type u_1}
{α : Type u_2}
[Collection β α]
{x : β}
{s : Finset β}
:
@[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
@[simp]