mathlib documentation

set_theory.lists

@[instance]
def lists'.decidable_eq (α : Type u) [a : decidable_eq α] (ᾰ : bool) :
inductive lists' (α : Type u) :
boolType u
def lists (α : Type u_1) :
Type 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 α)} (h : l₁ 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} (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_lista l₂
def lists.atom {α : Type u_1} (a : α) :
Equations
def lists.of' {α : Type u_1} (l : lists' α tt) :
Equations
@[simp]
def lists.to_list {α : Type u_1} :
lists αlist (lists α)
Equations
def lists.is_list {α : Type u_1} (l : lists α) :
Prop
Equations
def lists.of_list {α : Type u_1} (l : list (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) (C0 : Π (a : α), C (lists.atom a)) (C1 : Π (l : lists' α tt), D lC (lists.of' l)) (D0 : D lists'.nil) (D1 : Π (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} (a : 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} (s : l₁ l₂) :
a l₁a l₂
def finsets (α : Type u_1) :
Type 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