mathlib3 documentation

data.fin.tuple.reflection

Lemmas for tuples fin m → α #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains alternative definitions of common operators on vectors which expand definitionally to the expected expression when evaluated on ![] notation.

This allows "proof by reflection", where we prove f = ![f 0, f 1] by defining fin_vec.eta_expand f to be equal to the RHS definitionally, and then prove that f = eta_expand f.

The definitions in this file should normally not be used directly; the intent is for the corresponding *_eq lemmas to be used in a place where they are definitionally unfolded.

Main definitions #

source
def fin_vec.seq {α : Type u_1} {β : Type u_2} {m : ℕ} :
(fin m → α → β) → (fin m → α) → fin m → β

Evaluate fin_vec.seq f v = ![(f 0) (v 0), (f 1) (v 1), ...]

Equations
source
@[simp]
theorem fin_vec.seq_eq {α : Type u_1} {β : Type u_2} {m : ℕ} (f : fin m → α → β) (v : fin m → α) :
fin_vec.seq f v = λ (i : fin m), f i (v i)
source
def fin_vec.map {α : Type u_1} {β : Type u_2} (f : α → β) {m : ℕ} :
(fin m → α) → fin m → β

fin_vec.map f v = ![f (v 0), f (v 1), ...]

Equations
source
@[simp]
theorem fin_vec.map_eq {α : Type u_1} {β : Type u_2} (f : α → β) {m : ℕ} (v : fin m → α) :
fin_vec.map f v = f ∘ v

This can be use to prove

example {f : α → β} (a₁ a₂ : α) : f ∘ ![a₁, a₂] = ![f a₁, f a₂] :=
(map_eq _ _).symm
source
def fin_vec.eta_expand {α : Type u_1} {m : ℕ} (v : fin m → α) :
fin m → α

Expand v to ![v 0, v 1, ...]

Equations
source
@[simp]
theorem fin_vec.eta_expand_eq {α : Type u_1} {m : ℕ} (v : fin m → α) :
fin_vec.eta_expand v = v

This can be use to prove

example {f : α → β} (a : fin 2 → α) : a = ![a 0, a 1] := (eta_expand_eq _).symm
source
def fin_vec.forall {α : Type u_1} {m : ℕ} (P : (fin m → α) → Prop) :
Prop

∀ with better defeq for ∀ x : fin m → α, P x.

Equations
source
@[simp]
theorem fin_vec.forall_iff {α : Type u_1} {m : ℕ} (P : (fin m → α) → Prop) :
fin_vec.forall P ↔ ∀ (x : fin m → α), P x

This can be use to prove

example (P : (fin 2 → α) → Prop) : (∀ f, P f) ↔ (∀ a₀ a₁, P ![a₀, a₁]) := (forall_iff _).symm
source
def fin_vec.exists {α : Type u_1} {m : ℕ} (P : (fin m → α) → Prop) :
Prop

∃ with better defeq for ∃ x : fin m → α, P x.

Equations
source
theorem fin_vec.exists_iff {α : Type u_1} {m : ℕ} (P : (fin m → α) → Prop) :
fin_vec.exists P ↔ ∃ (x : fin m → α), P x

This can be use to prove

example (P : (fin 2 → α) → Prop) : (∃ f, P f) ↔ (∃ a₀ a₁, P ![a₀, a₁]) := (exists_iff _).symm
source
def fin_vec.sum {α : Type u_1} [has_add α] [has_zero α] {m : ℕ} (v : fin m → α) :
α

finset.univ.sum with better defeq for fin

Equations
source
@[simp]
theorem fin_vec.sum_eq {α : Type u_1} [add_comm_monoid α] {m : ℕ} (a : fin m → α) :
fin_vec.sum a = finset.univ.sum (λ (i : fin m), a i)

This can be used to prove

example [add_comm_monoid α] (a : fin 3 → α) : ∑ i, a i = a 0 + a 1 + a 2 :=
(sum_eq _).symm