LeanPool.PointwiseComposition.Foundation.Vorspiel.Matrix

Supporting results for pointwise provable equality.

The «term :> » construction in Matrix.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem PointwiseComposition.Matrix.vecCons_zero {α✝ : Type u_1} {a : α✝} {n✝ : ℕ} {s : Fin n✝ → α✝} :

(a :> s) 0 = a

source

theorem PointwiseComposition.Matrix.vecCons_succ {n : ℕ} {α✝ : Type u_1} {a : α✝} {s : Fin n → α✝} (i : Fin n) :

(a :> s) i.succ = s i

source

@[simp]

theorem PointwiseComposition.Matrix.vecCons_last {n : ℕ} {C : Type u_1} (a : C) (s : Fin (n + 1) → C) :

(a :> s) (Fin.last (n + 1)) = s (Fin.last n)

source

def PointwiseComposition.Matrix.vecConsLast {α : Type u} {n : ℕ} (t : Fin n → α) (h : α) :

Fin n.succ → α

The vec Cons Last construction in Matrix.

Equations

(t <: h) i = Fin.lastCases h t i

Instances For

source

@[simp]

theorem PointwiseComposition.Matrix.cons_app_one {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ → α) :

(a :> s) 1 = s 0

source

@[simp]

theorem PointwiseComposition.Matrix.cons_app_two {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ → α) :

(a :> s) 2 = s 1

source

@[simp]

theorem PointwiseComposition.Matrix.cons_app_three {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ → α) :

(a :> s) 3 = s 2

source

@[simp]

theorem PointwiseComposition.Matrix.cons_app_four {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ → α) :

(a :> s) 4 = s 3

source

@[simp]

theorem PointwiseComposition.Matrix.cons_app_five {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ → α) :

(a :> s) 5 = s 4

source

@[simp]

theorem PointwiseComposition.Matrix.cons_app_six {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ → α) :

(a :> s) 6 = s 5

source

@[simp]

theorem PointwiseComposition.Matrix.cons_app_seven {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ → α) :

(a :> s) 7 = s 6

source

@[simp]

theorem PointwiseComposition.Matrix.cons_app_eight {α : Type u} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ → α) :

(a :> s) 8 = s 7

source

def PointwiseComposition.Matrix.unexpandVecEmpty :

Lean.PrettyPrinter.Unexpander

The unexpand Vec Empty construction in Matrix.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def PointwiseComposition.Matrix.unexpandVecCons :

Lean.PrettyPrinter.Unexpander

The unexpand Vec Cons construction in Matrix.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def PointwiseComposition.Matrix.«term_<:_» :

Lean.TrailingParserDescr

The «term <: » construction in Matrix.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem PointwiseComposition.Matrix.rightConcat_last {n : ℕ} {α✝ : Type u_1} {s : Fin n → α✝} {a : α✝} :

(s <: a) (Fin.last n) = a

source

@[simp]

theorem PointwiseComposition.Matrix.rightConcat_castSucc {n : ℕ} {α✝ : Type u_1} {s : Fin n → α✝} {a : α✝} (i : Fin n) :

(s <: a) i.castSucc = s i

source

@[simp]

theorem PointwiseComposition.Matrix.rightConcat_zero {n : ℕ} {α : Type u} (a : α) (s : Fin n.succ → α) :

(s <: a) 0 = s 0

source

@[simp]

theorem PointwiseComposition.Matrix.zero_succ_eq_id {n : ℕ} :

0 :> Fin.succ = id

source

@[simp]

theorem PointwiseComposition.Matrix.zero_cons_succ_eq_self {n : ℕ} {α : Type u} (f : Fin (n + 1) → α) :

(f 0 :> fun (x : Fin n) => f x.succ) = f

source

theorem PointwiseComposition.Matrix.eq_vecCons {n : ℕ} {C : Type u_1} (s : Fin (n + 1) → C) :

s 0 :> s ∘ Fin.succ = s

source

theorem PointwiseComposition.Matrix.eq_vecCons' {n : ℕ} {C : Type u_1} (s : Fin (n + 1) → C) :

(s 0 :> fun (x : Fin n) => s x.succ) = s

source

theorem PointwiseComposition.Matrix.vecCons_ext {n : ℕ} {α : Type u} (a₁ a₂ : α) (s₁ s₂ : Fin n → α) :

a₁ :> s₁ = a₂ :> s₂ ↔ a₁ = a₂ ∧ s₁ = s₂

source

theorem PointwiseComposition.Matrix.vecCons_assoc {n : ℕ} {α : Type u} (a b : α) (s : Fin n → α) :

a :> s <: b = (a :> s) <: b

source

def PointwiseComposition.Matrix.decVec {α : Type u_1} {n : ℕ} (v w : Fin n → α) :

((i : Fin n) → Decidable (v i = w i)) → Decidable (v = w)

The dec Vec construction in Matrix.

Equations

PointwiseComposition.Matrix.decVec x_4 x_5 x_6 = ⋯.mpr (isTrue trivial)
PointwiseComposition.Matrix.decVec v w d = ⋯.mpr (⋯.mpr (⋯.mpr instDecidableAnd))

Instances For

source

theorem PointwiseComposition.Matrix.comp_vecCons {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (a : α) (s : Fin n → α) :

(fun (x : Fin n.succ) => f ((a :> s) x)) = f a :> f ∘ s

source

theorem PointwiseComposition.Matrix.comp_vecCons' {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (a : α) (s : Fin n → α) :

(fun (x : Fin n.succ) => f ((a :> s) x)) = f a :> fun (i : Fin n) => f (s i)

source

theorem PointwiseComposition.Matrix.comp_vecCons'' {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (a : α) (s : Fin n → α) :

f ∘ (a :> s) = f a :> f ∘ s

source

theorem PointwiseComposition.Matrix.comp_vecCons₂' {n : ℕ} {α : Type u} {β : Sort u_1} {γ : Type u_2} (g : β → γ) (f : α → β) (a : α) (s : Fin n → α) :

(fun (x : Fin n.succ) => g (f ((a :> s) x))) = g (f a) :> fun (i : Fin n) => g (f (s i))

source

@[simp]

theorem PointwiseComposition.Matrix.comp₀ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} :

f ∘ ![] = ![]

source

@[simp]

theorem PointwiseComposition.Matrix.comp₁ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} (a : α) :

f ∘ ![a] = ![f a]

source

@[simp]

theorem PointwiseComposition.Matrix.comp₂ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} (a₁ a₂ : α) :

f ∘ ![a₁, a₂] = ![f a₁, f a₂]

source

@[simp]

theorem PointwiseComposition.Matrix.comp₃ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} (a₁ a₂ a₃ : α) :

f ∘ ![a₁, a₂, a₃] = ![f a₁, f a₂, f a₃]

source

@[simp]

theorem PointwiseComposition.Matrix.comp₄ {α : Type u} {δ✝ : Type u_1} {f : α → δ✝} (a₁ a₂ a₃ a₄ : α) :

f ∘ ![a₁, a₂, a₃, a₄] = ![f a₁, f a₂, f a₃, f a₄]

source

theorem PointwiseComposition.Matrix.comp_vecConsLast {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (a : α) (s : Fin n → α) :

(fun (x : Fin n.succ) => f ((s <: a) x)) = f ∘ s <: f a

source

@[simp]

theorem PointwiseComposition.Matrix.vecHead_comp {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (v : Fin (n + 1) → α) :

Matrix.vecHead (f ∘ v) = f (Matrix.vecHead v)

source

@[simp]

theorem PointwiseComposition.Matrix.vecTail_comp {n : ℕ} {α : Type u} {β : Type u_1} (f : α → β) (v : Fin (n + 1) → α) :

Matrix.vecTail (f ∘ v) = f ∘ Matrix.vecTail v

source

theorem PointwiseComposition.Matrix.vecConsLast_vecEmpty {α : Type u} {s : Fin 0 → α} (a : α) :

s <: a = ![a]

source

theorem PointwiseComposition.Matrix.constant_eq_singleton {α : Type u} {a : α} :

(fun (x : Fin (Nat.succ 0)) => a) = ![a]

source

theorem PointwiseComposition.Matrix.fun_eq_vec_one {α : Type u} (v : Fin 1 → α) :

v = ![v 0]

source

theorem PointwiseComposition.Matrix.constant_eq_vec₂ {α : Type u} {a : α} :

(fun (x : Fin (Nat.succ 0).succ) => a) = ![a, a]

source

theorem PointwiseComposition.Matrix.fun_eq_vec_two {α : Type u} (v : Fin 2 → α) :

v = ![v 0, v 1]

source

theorem PointwiseComposition.Matrix.fun_eq_vec_three {α : Type u} (v : Fin 3 → α) :

v = ![v 0, v 1, v 2]

source

theorem PointwiseComposition.Matrix.fun_eq_vec_four {α : Type u} (v : Fin 4 → α) :

v = ![v 0, v 1, v 2, v 3]

source

theorem PointwiseComposition.Matrix.fun_eq_vec_four' {α : Type u} {β : Type u_1} (f : α → β) (v : Fin 4 → α) :

f ∘ v = ![f (v 0), f (v 1), f (v 2), f (v 3)]

source

theorem PointwiseComposition.Matrix.injective_vecCons {n : ℕ} {α : Type u} {f : Fin n → α} (h : Function.Injective f) {a : α} (ha : ∀ (i : Fin n), a ≠ f i) :

Function.Injective (a :> f)

source

@[simp]

theorem PointwiseComposition.Matrix.vecCons_empty_eq_singleton {α : Type u} (v : Fin 0 → α) (x : α) :

x :> v = ![x]

source

@[simp]

theorem PointwiseComposition.Matrix.vecConsLast_empty_eq_singleton {α : Type u} (v : Fin 0 → α) (x : α) :

v <: x = ![x]

source

def PointwiseComposition.Matrix.toList {α : Type u_1} {n : ℕ} :

(Fin n → α) → List α

The to List construction in Matrix.

Equations

PointwiseComposition.Matrix.toList x_2 = []
PointwiseComposition.Matrix.toList v = v 0 :: PointwiseComposition.Matrix.toList (v ∘ Fin.succ)

Instances For

source

@[simp]

theorem PointwiseComposition.Matrix.toList_zero {α : Type u_1} (v : Fin 0 → α) :

toList v = []

source

@[simp]

theorem PointwiseComposition.Matrix.toList_succ {α : Type u_1} {n : ℕ} (v : Fin (n + 1) → α) :

toList v = v 0 :: toList (v ∘ Fin.succ)

source

@[simp]

theorem PointwiseComposition.Matrix.toList_length {α : Type u_1} {n : ℕ} (v : Fin n → α) :

(toList v).length = n

source

@[simp]

theorem PointwiseComposition.Matrix.mem_toList_iff {α : Type u_1} {n : ℕ} {v : Fin n → α} {a : α} :

a ∈ toList v ↔ ∃ (i : Fin n), v i = a

source

def PointwiseComposition.Matrix.getM {m : Type u → Type v} [Monad m] {n : ℕ} {β : Fin n → Type u} :

((i : Fin n) → m (β i)) → m ((i : Fin n) → β i)

The get M construction in Matrix.

Equations

One or more equations did not get rendered due to their size.
PointwiseComposition.Matrix.getM x_4 = pure finZeroElim

Instances For

source

theorem PointwiseComposition.Matrix.getM_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {n : ℕ} {β : Fin n → Type u} (v : (i : Fin n) → β i) :

(getM fun (i : Fin n) => pure (v i)) = pure v

source

@[simp]

theorem PointwiseComposition.Matrix.getM_some {n : ℕ} {β : Fin n → Type u} (v : (i : Fin n) → β i) :

(getM fun (i : Fin n) => some (v i)) = some v

source

def PointwiseComposition.Matrix.appendr {α : Type w} {n m : ℕ} (v : Fin n → α) (w : Fin m → α) :

Fin (m + n) → α

The appendr construction in Matrix.

Equations

PointwiseComposition.Matrix.appendr v w = Matrix.vecAppend ⋯ v w

Instances For

source

@[simp]

theorem PointwiseComposition.Matrix.appendr_nil {α : Type w} {m : ℕ} (w : Fin m → α) :

appendr ![] w = w

source

@[simp]

theorem PointwiseComposition.Matrix.appendr_cons {α : Type w} {m n : ℕ} (x : α) (v : Fin n → α) (w : Fin m → α) :

appendr (x :> v) w = x :> appendr v w

source

theorem PointwiseComposition.Matrix.vecForall_iff {α : Type w} {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) :

(∀ (v : Fin (n + 1) → α), φ v) ↔ ∀ (a : α) (v : Fin n → α), φ (a :> v)

source

theorem PointwiseComposition.Matrix.vecExists_iff {α : Type w} {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) :

(∃ (v : Fin (n + 1) → α), φ v) ↔ ∃ (a : α) (v : Fin n → α), φ (a :> v)

source

def PointwiseComposition.Matrix.foldr {α : Type w} {β : Type u} (f : α → β → β) (init : β) {k : ℕ} :

(Fin k → α) → β

The foldr construction in Matrix.

Equations

PointwiseComposition.Matrix.foldr f init x_2 = init
PointwiseComposition.Matrix.foldr f init v = f (Matrix.vecHead v) (PointwiseComposition.Matrix.foldr f init (Matrix.vecTail v))

Instances For

source

def PointwiseComposition.Matrix.vecMap {α : Type w} {β : Type u} {k : ℕ} (f : α → β) :

(Fin k → α) → Fin k → β

The vec Map construction in Matrix.

Equations

f↗ v = f ∘ v

Instances For

source

def PointwiseComposition.Matrix.«term_↗» :

Lean.TrailingParserDescr

The «term ↗» construction in Matrix.

Equations

PointwiseComposition.Matrix.«term_↗» = Lean.ParserDescr.trailingNode `PointwiseComposition.Matrix.«term_↗» 1024 1024 (Lean.ParserDescr.symbol "↗")

Instances For

source

@[simp]

theorem PointwiseComposition.Matrix.vecMap_nil {α : Type w} {β : Type u} (f : α → β) (v : Fin 0 → α) :

f↗ v = ![]

source

theorem PointwiseComposition.Matrix.vecMap_cons {α : Type w} {β : Type u} (f : α → β) {k : ℕ} (a : α) (v : Fin k → α) :

f↗ (a :> v) = f a :> f↗ v

source

@[simp]

theorem PointwiseComposition.Matrix.vecMap_cons' {α : Type w} {β : Type u} (f : α → β) {k : ℕ} (v : Fin (k + 1) → α) :

f↗ v = f (Matrix.vecHead v) :> f↗ (Matrix.vecTail v)

source

@[simp]

theorem PointwiseComposition.Matrix.vecMap_app {α : Type w} {β : Type u} (f : α → β) {k : ℕ} (v : Fin k → α) (i : Fin k) :

f↗ v i = f (v i)

source

theorem PointwiseComposition.Matrix.vecMap_vecMap_comp {α : Type w} {β : Type u} {γ : Type u_1} {k : ℕ} (g : β → γ) (f : α → β) (v : Fin k → α) :

g↗ (f↗ v) = (g ∘ f)↗ v

source

theorem PointwiseComposition.Matrix.vecMap_vecMap_comp' {α : Type w} {β : Type u} {γ : Type u_1} {k : ℕ} (g : β → γ) (f : α → β) (v : Fin k → α) :

g↗ (f↗ v) = (fun (x : α) => g (f x))↗ v

source

@[simp]

theorem PointwiseComposition.Matrix.foldr_zero {α : Type w} {β : Type u} (f : α → β → β) (init : β) (v : Fin 0 → α) :

foldr f init v = init

source

@[simp]

theorem PointwiseComposition.Matrix.foldr_succ {α : Type w} {β : Type u} (f : α → β → β) (init : β) {k : ℕ} (v : Fin (k + 1) → α) :

foldr f init v = f (Matrix.vecHead v) (foldr f init (Matrix.vecTail v))

source

def PointwiseComposition.Matrix.foldl {α : Type w} {β : Type u} (f : α → β → α) (init : α) {k : ℕ} :

(Fin k → β) → α

The foldl construction in Matrix.

Equations

PointwiseComposition.Matrix.foldl f x✝ x_3 = x✝
PointwiseComposition.Matrix.foldl f x✝ v = PointwiseComposition.Matrix.foldl f (f x✝ (Matrix.vecHead v)) (Matrix.vecTail v)

Instances For

source

@[simp]

theorem PointwiseComposition.Matrix.foldl_zero {α : Type w} {β : Type u} (f : α → β → α) (init : α) (v : Fin 0 → β) :

foldl f init v = init

source

@[simp]

theorem PointwiseComposition.Matrix.foldl_succ {α : Type w} {β : Type u} (f : α → β → α) (init : α) {k : ℕ} (v : Fin (k + 1) → β) :

foldl f init v = foldl f (f init (Matrix.vecHead v)) (Matrix.vecTail v)

source

theorem PointwiseComposition.Matrix.eq_iff_eq_vecHead_of_eq_vecTail {α : Type w} {n : ℕ} {v₁ v₂ : Fin (n + 1) → α} :

Matrix.vecHead v₁ = Matrix.vecHead v₂ ∧ Matrix.vecTail v₁ = Matrix.vecTail v₂ ↔ v₁ = v₂

source

def PointwiseComposition.Matrix.vecToNat {n : ℕ} (v : Fin n → ℕ) :

ℕ

The vec To Nat construction in Matrix.

Equations

PointwiseComposition.Matrix.vecToNat v = PointwiseComposition.Matrix.foldr (fun (x ih : ℕ) => Nat.pair x ih + 1) 0 v

Instances For

source

@[simp]

theorem PointwiseComposition.Matrix.vecToNat_empty (v : Fin 0 → ℕ) :

vecToNat v = 0

source

@[simp]

theorem PointwiseComposition.Matrix.encode_succ {n : ℕ} (x : ℕ) (v : Fin n → ℕ) :

vecToNat (x :> v) = Nat.pair x (vecToNat v) + 1

source

@[simp]

theorem PointwiseComposition.Matrix.appeendr_addCast {α : Type w} {m n : ℕ} (u : Fin m → α) (v : Fin n → α) (i : Fin m) :

appendr u v (Fin.addCast n i) = u i

source

@[simp]

theorem PointwiseComposition.Matrix.appeendr_addNat {α : Type w} {m n : ℕ} (u : Fin m → α) (v : Fin n → α) (i : Fin n) :

appendr u v (i.addNat m) = v i