mathlib documentation

set_theory.lists

@[instance]
def lists'.decidable_eq (α : Type u) [a : decidable_eq α] (ᾰ : bool) :

inductive lists'  :
Type uboolType u

def lists  :
Type u_1Type u_1

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

Equations
def lists'.cons {α : Type u_1} :
lists αlists' α ttlists' α tt

Equations
@[simp]
def lists'.to_list {α : Type u_1} {b : bool} :
lists' α blist (lists α)

Equations
@[simp]
theorem lists'.to_list_cons {α : Type u_1} (a : lists α) (l : lists' α tt) :

@[simp]
def lists'.of_list {α : Type u_1} :
list (lists α)lists' α tt

Equations
@[simp]
theorem lists'.to_of_list {α : Type u_1} (l : list (lists α)) :

@[simp]
theorem lists'.of_to_list {α : Type u_1} (l : lists' α tt) :

@[instance]
def lists'.has_subset {α : Type u_1} :

Equations
@[instance]
def lists'.has_mem {α : Type u_1} {b : bool} :
has_mem (lists α) (lists' α b)

Equations
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 α)} :
l₁ l₂lists'.of_list l₁ lists'.of_list l₂

theorem lists'.subset_nil {α : Type u_1} {l : lists' α tt} :

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

theorem lists'.subset_def {α : Type u_1} {l₁ l₂ : lists' α tt} :
l₁ l₂ ∀ (a : lists α), a l₁.to_lista l₂

def lists.atom {α : Type u_1} :
α → lists α

Equations
def lists.of' {α : Type u_1} :
lists' α ttlists α

Equations
@[simp]
def lists.to_list {α : Type u_1} :
lists αlist (lists α)

Equations
def lists.is_list {α : Type u_1} :
lists α → Prop

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

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

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

theorem lists.of_to_list {α : Type u_1} {l : lists α} :

@[instance]
def lists.inhabited {α : Type u_1} :

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

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

Equations
def lists.induction_mut {α : Type u_1} (C : lists αSort u_2) (D : lists' α ttSort u_3) :
(Π (a : α), C (lists.atom a))(Π (l : lists' α tt), D lC (lists.of' l))D lists'.nil(Π (a : lists α) (l : lists' α tt), C aD lD (lists'.cons a l))pprod (Π (l : lists α), C l) (Π (l : lists' α tt), D l)

Equations
def lists.mem {α : Type u_1} :
lists αlists α → Prop

Equations
@[instance]
def lists.has_mem {α : Type u_1} :
has_mem (lists α) (lists α)

Equations
theorem lists.is_list_of_mem {α : Type u_1} {a l : lists α} :
a l → l.is_list

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

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

theorem lists.lt_sizeof_cons' {α : Type u_1} {b : bool} (a : lists' α b) (l : lists' α tt) :
sizeof b, a⟩ < sizeof (a.cons' l)

@[instance]
def lists.mem.decidable {α : Type u_1} [decidable_eq α] (a : lists α) (l : lists' α tt) :

Equations
@[instance]
def lists.subset.decidable {α : Type u_1} [decidable_eq α] (l₁ l₂ : lists' α tt) :
decidable (l₁ l₂)

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

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

def finsets  :
Type u_1Type u_1

Equations
@[instance]
def finsets.has_emptyc {α : Type u_1} :

Equations
@[instance]
def finsets.inhabited {α : Type u_1} :

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

Equations