LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.FinLists

Auxiliary declarations for the Borel determinacy formalization.

@[simp]

theorem List.append_compose {α : Type u_1} (x y : List α) : ((fun (x_1 : List α) => x ++ x_1) ∘ fun (x : List α) => y ++ x) = fun (x_1 : List α) => x ++ y ++ x_1

@[simp]

theorem List.subAtFin_append {α : Type u_1} (T : Set (List α)) (x y : List α) : (fun (x : List α) => y ++ x) ⁻¹' (fun (x_1 : List α) => x ++ x_1) ⁻¹' T = (fun (x_1 : List α) => x ++ y ++ x_1) ⁻¹' T

theorem List.eq_take_concat {α : Type u_1} (x : List α) (n : ℕ) (h : x.length = n + 1) : x = take n x ++ [x[n]]

theorem List.head_eq_get {α : Type u_1} (x : List α) (h : x ≠ []) : x.head h = x[0]

theorem List.tail_eq_drop {α : Type u_1} (x : List α) : x.tail = drop 1 x

theorem List.tail_take {α : Type u_1} {n : ℕ} (x : List α) : (take (n + 1) x).tail = take n x.tail

theorem List.head_tail_take {α : Type u_1} {n : ℕ} (x : List α) (h : x ≠ []) : x.head h :: take n x.tail = take (n + 1) x

theorem List.tail_getElem {α : Type u_1} (x : List α) (n : ℕ) (h : n < x.tail.length) : x.tail[n] = x[n + 1]

theorem List.zipWith_left {α : Type u_1} {β : Type u_2} (x : List α) (z : List β) : zipWith (fun (a : α) (x : β) => a) x z = take z.length x

@[reducible, inline]

abbrev List.mapEval {α : Type u_4} {β : α → Type u_5} (a : α) (x : List ((a : α) → β a)) : List (β a)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• List.mapEval a x = List.map (fun (f : (a : α) → β a) => f a) x

def List.zipFun {α : Type u_4} {β : α → Type u_5} {n : ℕ} (f : (a : α) → List (β a)) (h : ∀ (a : α), (f a).length = n) : List ((a : α) → β a)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• List.zipFun f h_2 = []
• List.zipFun f h_2 = (fun (a : α) => (f a).head ⋯) :: List.zipFun (fun (a : α) => (f a).tail) ⋯

@[simp]

theorem List.mapEval_zip {α : Type u_1} {a : α} {n : ℕ} {β : α → Type u_4} (f : (a : α) → List (β a)) (h : ∀ (a : α), (f a).length = n) : mapEval a (zipFun f h) = f a

@[simp]

theorem List.zip_mapEval {α : Type u_1} {β : α → Type u_4} (x : List ((a : α) → β a)) : zipFun (fun (a : α) => mapEval a x) ⋯ = x

theorem List.mapEval_joint_epi {α : Type u_1} {β : α → Type u_4} {x y : List ((a : α) → β a)} (hl : x.length = y.length) (h : ∀ (a : α), mapEval a x = mapEval a y) : x = y

@[simp]

theorem List.zipFun_len {α : Type u_1} {n : ℕ} {β : α → Type u_4} (f : (a : α) → List (β a)) (h : ∀ (a : α), (f a).length = n) : (zipFun f h).length = n

@[simp]

theorem List.zipFun_zero {α : Type u_1} {β : α → Type u_4} (f : (a : α) → List (β a)) (h : ∀ (a : α), (f a).length = 0) : zipFun f h = []

@[simp]

theorem List.zipFun_append {α : Type u_1} {m n : ℕ} {β : α → Type u_4} (f g : (a : α) → List (β a)) (hf : ∀ (a : α), (f a).length = m) (hg : ∀ (a : α), (g a).length = n) : zipFun f hf ++ zipFun g hg = zipFun (fun (a : α) => f a ++ g a) ⋯

theorem List.zipFun_mono {α : Type u_1} {m n : ℕ} {β : α → Type u_4} (f g : (a : α) → List (β a)) (hf : ∀ (a : α), (f a).length = m) (hg : ∀ (a : α), (g a).length = n) (hm : m ≤ n) (h : ∀ (a : α), f a <+: g a) : zipFun f hf <+: zipFun g hg

def List.zipInitsMap {α : Type u_1} {β : Type u_2} (x : List α) (f : α → List α → β) : List β

Auxiliary declaration for the Borel determinacy formalization.

Equations

• x.zipInitsMap f = List.zipWith f x x.inits.tail

@[simp]

theorem List.zipInitsMap_nil {α : Type u_1} {β : Type u_2} (f : α → List α → β) : [].zipInitsMap f = []

@[simp]

theorem List.zipInitsMap_singleton {α : Type u_1} {β : Type u_2} (a : α) (f : α → List α → β) : [a].zipInitsMap f = [f a [a]]

theorem List.zipInitsMap_append {α : Type u_1} {β : Type u_2} (x y : List α) (f : α → List α → β) : (x ++ y).zipInitsMap f = x.zipInitsMap f ++ y.zipInitsMap fun (a : α) (z : List α) => f a (x ++ z)

theorem List.IsPrefix.zipInitsMap {α : Type u_1} {β : Type u_2} (x y : List α) (f : α → List α → β) (h : x <+: y) : x.zipInitsMap f <+: y.zipInitsMap f

@[simp]

theorem List.zipInitsMap_concat {α : Type u_1} {β : Type u_2} (x : List α) (a : α) (f : α → List α → β) : (x ++ [a]).zipInitsMap f = x.zipInitsMap f ++ [f a (x ++ [a])]

@[simp]

theorem List.zipInitsMap_length {α : Type u_1} {β : Type u_2} (x : List α) (f : α → List α → β) : (x.zipInitsMap f).length = x.length

theorem List.zipInitsMap_take {α : Type u_1} {β : Type u_2} {n : ℕ} (x : List α) (f : α → List α → β) : take n (x.zipInitsMap f) = (take n x).zipInitsMap f

theorem List.map_zipInitsMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : List α) (f : α → β) (g : β → List β → γ) : (x.zipInitsMap fun (a : α) (y : List α) => g (f a) (map f y)) = (map f x).zipInitsMap g

theorem List.zipInitsMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : List α) (f : α → List α → β) (g : β → γ) : (x.zipInitsMap fun (a : α) (b : List α) => g (f a b)) = map g (x.zipInitsMap f)

@[simp]

theorem List.zipInitsMap_eq_map {α : Type u_1} {β : Type u_2} (x : List α) (g : α → β) : (x.zipInitsMap fun (a : α) (x : List α) => g a) = map g x

@[simp]

theorem List.zipInitsMap_get {α : Type u_1} {β : Type u_2} (x : List α) (f : α → List α → β) (n : ℕ) (h : n < (x.zipInitsMap f).length) : (x.zipInitsMap f)[n] = f x[n] (take (n + 1) x)