mathlib documentation

set_theory.lists

@[instance]

def lists'.decidable_eq (α : Type u) [a : decidable_eq α] (a_1 : bool) :

decidable_eq (lists' α a_1)

inductive lists' (α : Type u) (a : bool) :

Type u

atom : Π (α : Type u), α → lists' α ff
nil : Π (α : Type u), lists' α tt
cons' : Π (α : Type u) {b : bool}, lists' α b → lists' α tt → lists' α tt

def lists (α : Type u_1) :

Type u_1

Equations

lists α = Σ (b : bool), lists' α b

@[instance]

def lists'.inhabited {α : Type u_1} [inhabited α] (b : bool) :

inhabited (lists' α b)

Equations

lists'.inhabited tt = {default := lists'.nil α}
lists'.inhabited ff = {default := lists'.atom (default α)}

def lists'.cons {α : Type u_1} (a : lists α) (a_1 : lists' α tt) :

Equations

lists'.cons ⟨b, a⟩ l = a.cons' l

@[simp]

def lists'.to_list {α : Type u_1} {b : bool} (a : lists' α b) :

list (lists α)

Equations

(a.cons' l).to_list = ⟨a_6, a⟩ :: l.to_list
lists'.nil.to_list = list.nil
(lists'.atom a).to_list = list.nil

@[simp]

theorem lists'.to_list_cons {α : Type u_1} (a : lists α) (l : lists' α tt) :

(lists'.cons a l).to_list = a :: l.to_list

@[simp]

def lists'.of_list {α : Type u_1} (a : list (lists α)) :

Equations

lists'.of_list (a :: l) = lists'.cons a (lists'.of_list l)
lists'.of_list list.nil = lists'.nil

@[simp]

theorem lists'.to_of_list {α : Type u_1} (l : list (lists α)) :

(lists'.of_list l).to_list = l

@[simp]

theorem lists'.of_to_list {α : Type u_1} (l : lists' α tt) :

lists'.of_list l.to_list = l

@[instance]

def lists'.has_subset {α : Type u_1} :

has_subset (lists' α tt)

Equations

lists'.has_subset = {subset := lists'.subset α}

@[instance]

def lists'.has_mem {α : Type u_1} {b : bool} :

has_mem (lists α) (lists' α b)

Equations

lists'.has_mem = {mem := λ (a : lists α) (l : lists' α b), ∃ (a' : lists α) (H : a' ∈ l.to_list), a.equiv a'}

theorem lists'.mem_def {α : Type u_1} {b : bool} {a : lists α} {l : lists' α b} :

a ∈ l ↔ ∃ (a' : lists α) (H : a' ∈ l.to_list), a.equiv a'

@[simp]

theorem lists'.mem_cons {α : Type u_1} {a y : lists α} {l : lists' α tt} :

a ∈ lists'.cons y l ↔ a.equiv y ∨ a ∈ l

theorem lists'.cons_subset {α : Type u_1} {a : lists α} {l₁ l₂ : lists' α tt} :

lists'.cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

theorem lists'.of_list_subset {α : Type u_1} {l₁ l₂ : list (lists α)} (h : l₁ ⊆ l₂) :

lists'.of_list l₁ ⊆ lists'.of_list l₂

theorem lists'.subset_nil {α : Type u_1} {l : lists' α tt} (a : l ⊆ lists'.nil) :

theorem lists'.mem_of_subset' {α : Type u_1} {a : lists α} {l₁ l₂ : lists' α tt} (s : l₁ ⊆ l₂) (h : a ∈ l₁.to_list) :

a ∈ l₂

theorem lists'.subset_def {α : Type u_1} {l₁ l₂ : lists' α tt} :

l₁ ⊆ l₂ ↔ ∀ (a : lists α), a ∈ l₁.to_list → a ∈ l₂

def lists.atom {α : Type u_1} (a : α) :

Equations

lists.atom a = ⟨ff, lists'.atom a⟩

def lists.of' {α : Type u_1} (l : lists' α tt) :

Equations

lists.of' l = ⟨tt, l⟩

@[simp]

def lists.to_list {α : Type u_1} (a : lists α) :

list (lists α)

Equations

lists.to_list ⟨b, l⟩ = l.to_list

def lists.is_list {α : Type u_1} (l : lists α) :

Prop

Equations

l.is_list = ↥(l.fst)

def lists.of_list {α : Type u_1} (l : list (lists α)) :

Equations

lists.of_list l = lists.of' (lists'.of_list l)

theorem lists.is_list_to_list {α : Type u_1} (l : list (lists α)) :

(lists.of_list l).is_list

theorem lists.to_of_list {α : Type u_1} (l : list (lists α)) :

(lists.of_list l).to_list = l

theorem lists.of_to_list {α : Type u_1} {l : lists α} (a : l.is_list) :

lists.of_list l.to_list = l

@[instance]

def lists.inhabited {α : Type u_1} :

inhabited (lists α)

Equations

lists.inhabited = {default := lists.of' lists'.nil}

@[instance]

def lists.decidable_eq {α : Type u_1} [decidable_eq α] :

decidable_eq (lists α)

Equations

lists.decidable_eq = lists.decidable_eq._proof_1.mpr (λ (a b : Σ (b : bool), lists' α b), sigma.decidable_eq a b)

@[instance]

def lists.has_sizeof {α : Type u_1} [has_sizeof α] :

has_sizeof (lists α)

Equations

lists.has_sizeof = lists.has_sizeof._proof_1.mpr (sigma.has_sizeof bool (λ (b : bool), lists' α b))

def lists.induction_mut {α : Type u_1} (C : lists α → Sort u_2) (D : lists' α tt → Sort u_3) (C0 : Π (a : α), C (lists.atom a)) (C1 : Π (l : lists' α tt), D l → C (lists.of' l)) (D0 : D lists'.nil) (D1 : Π (a : lists α) (l : lists' α tt), C a → D l → D (lists'.cons a l)) :

pprod (Π (l : lists α), C l) (Π (l : lists' α tt), D l)

Equations

lists.induction_mut C D C0 C1 D0 D1 = ⟨λ (_x : lists α), lists.induction_mut._match_2 C D (λ (b : bool) (l : lists' α b), lists'.rec (λ (a : α), ⟨C0 a, punit.star⟩) ⟨C1 lists'.nil D0, D0⟩ (λ {b : bool} (a : lists' α b) (l : lists' α tt) (IH₁ : pprod (C ⟨b, a⟩) (lists.induction_mut._match_1 D b a)) (IH₂ : pprod (C ⟨tt, l⟩) (lists.induction_mut._match_1 D tt l)), ⟨C1 (a.cons' l) (D1 ⟨b, a⟩ l IH₁.fst IH₂.snd), D1 ⟨b, a⟩ l IH₁.fst IH₂.snd⟩) l) _x, λ (l : lists' α tt), ((λ (b : bool) (l : lists' α b), lists'.rec (λ (a : α), ⟨C0 a, punit.star⟩) ⟨C1 lists'.nil D0, D0⟩ (λ {b : bool} (a : lists' α b) (l : lists' α tt) (IH₁ : pprod (C ⟨b, a⟩) (lists.induction_mut._match_1 D b a)) (IH₂ : pprod (C ⟨tt, l⟩) (lists.induction_mut._match_1 D tt l)), ⟨C1 (a.cons' l) (D1 ⟨b, a⟩ l IH₁.fst IH₂.snd), D1 ⟨b, a⟩ l IH₁.fst IH₂.snd⟩) l) tt l).snd⟩
lists.induction_mut._match_2 C D this ⟨b, l⟩ = (this l).fst
lists.induction_mut._match_1 D tt l = D l
lists.induction_mut._match_1 D ff l = punit

def lists.mem {α : Type u_1} (a a_1 : lists α) :

Prop

Equations

a.mem ⟨tt, l⟩ = (a ∈ l)
a.mem ⟨ff, l⟩ = false

@[instance]

def lists.has_mem {α : Type u_1} :

has_mem (lists α) (lists α)

Equations

lists.has_mem = {mem := lists.mem α}

theorem lists.is_list_of_mem {α : Type u_1} {a l : lists α} (a_1 : a ∈ l) :

theorem lists.equiv_atom {α : Type u_1} {a : α} {l : lists α} :

(lists.atom a).equiv l ↔ lists.atom a = l

@[instance]

def lists.setoid {α : Type u_1} :

setoid (lists α)

Equations

lists.setoid = {r := lists.equiv α, iseqv := _}

theorem lists.sizeof_pos {α : Type u_1} {b : bool} (l : lists' α b) :

theorem lists.lt_sizeof_cons' {α : Type u_1} {b : bool} (a : lists' α b) (l : lists' α tt) :

sizeof ⟨b, a⟩ < sizeof (a.cons' l)

theorem lists'.mem_equiv_left {α : Type u_1} {l : lists' α tt} {a a' : lists α} (a_1 : a.equiv a') :

a ∈ l ↔ a' ∈ l

theorem lists'.mem_of_subset {α : Type u_1} {a : lists α} {l₁ l₂ : lists' α tt} (s : l₁ ⊆ l₂) (a_1 : a ∈ l₁) :

a ∈ l₂

def finsets (α : Type u_1) :

Type u_1

Equations

finsets α = quotient lists.setoid

@[instance]

def finsets.has_emptyc {α : Type u_1} :

has_emptyc (finsets α)

Equations

finsets.has_emptyc = {emptyc := ⟦lists.of' lists'.nil⟧}

@[instance]

def finsets.inhabited {α : Type u_1} :

inhabited (finsets α)

Equations

finsets.inhabited = {default := ∅}

@[instance]

def finsets.decidable_eq {α : Type u_1} [decidable_eq α] :

decidable_eq (finsets α)

Equations

finsets.decidable_eq = finsets.decidable_eq._proof_1.mpr (λ (a b : quotient lists.setoid), quotient.decidable_eq a b)