mathlib3 documentation

data.typevec

Tuples of types, and their categorical structure. #

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

Features #

Also, support functions for operating with n-tuples of types, such as:

Since e.g. append1 α.drop α.last is propositionally equal to α but not definitionally equal to it, we need support functions and lemmas to mediate between constructions.

source
def typevec (n : ℕ) :
Type (u_1+1)

n-tuples of types, as a category

Equations
Instances for typevec
source
@[protected, instance]
def typevec.inhabited {n : ℕ} :
inhabited (typevec n)
Equations
source
def typevec.arrow {n : ℕ} (α : typevec n) (β : typevec n) :
Type (max u_1 u_2)

arrow in the category of typevec

Equations
Instances for typevec.arrow
source
@[protected, instance]
def typevec.arrow.inhabited {n : ℕ} (α : typevec n) (β : typevec n) [Π (i : fin2 n), inhabited (β i)] :
inhabited (α.arrow β)
Equations
source
def typevec.id {n : ℕ} {α : typevec n} :
α.arrow α

identity of arrow composition

Equations
source
def typevec.comp {n : ℕ} {α : typevec n} {β : typevec n} {γ : typevec n} (g : β.arrow γ) (f : α.arrow β) :
α.arrow γ

arrow composition in the category of typevec

Equations
source
@[simp]
theorem typevec.id_comp {n : ℕ} {α : typevec n} {β : typevec n} (f : α.arrow β) :
typevec.comp typevec.id f = f
source
@[simp]
theorem typevec.comp_id {n : ℕ} {α : typevec n} {β : typevec n} (f : α.arrow β) :
typevec.comp f typevec.id = f
source
theorem typevec.comp_assoc {n : ℕ} {α : typevec n} {β : typevec n} {γ : typevec n} {δ : typevec n} (h : γ.arrow δ) (g : β.arrow γ) (f : α.arrow β) :
typevec.comp (typevec.comp h g) f = typevec.comp h (typevec.comp g f)
source
def typevec.append1 {n : ℕ} (α : typevec n) (β : Type u_1) :
typevec (n + 1)

Support for extending a typevec by one element.

Equations
source
def typevec.drop {n : ℕ} (α : typevec (n + 1)) :
typevec n

retain only a n-length prefix of the argument

Equations
source
def typevec.last {n : ℕ} (α : typevec (n + 1)) :
Type u

take the last value of a (n+1)-length vector

Equations
Instances for typevec.last
source
@[protected, instance]
def typevec.last.inhabited {n : ℕ} (α : typevec (n + 1)) [inhabited (α fin2.fz)] :
inhabited α.last
Equations
source
theorem typevec.drop_append1 {n : ℕ} {α : typevec n} {β : Type u_1} {i : fin2 n} :
(α ::: β).drop i = α i
source
@[simp]
theorem typevec.drop_append1' {n : ℕ} {α : typevec n} {β : Type u_1} :
(α ::: β).drop = α
source
theorem typevec.last_append1 {n : ℕ} {α : typevec n} {β : Type u_1} :
(α ::: β).last = β
source
@[simp]
theorem typevec.append1_drop_last {n : ℕ} (α : typevec (n + 1)) :
α.drop ::: α.last = α
source
def typevec.append1_cases {n : ℕ} {C : typevec (n + 1) → Sort u} (H : Π (α : typevec n) (β : Type u_1), C (α ::: β)) (γ : typevec (n + 1)) :
C γ

cases on (n+1)-length vectors

Equations
source
@[simp]
theorem typevec.append1_cases_append1 {n : ℕ} {C : typevec (n + 1) → Sort u} (H : Π (α : typevec n) (β : Type u_1), C (α ::: β)) (α : typevec n) (β : Type u_1) :
typevec.append1_cases H (α ::: β) = H α β
source
def typevec.split_fun {n : ℕ} {α : typevec (n + 1)} {α' : typevec (n + 1)} (f : α.drop.arrow α'.drop) (g : α.last → α'.last) :
α.arrow α'

append an arrow and a function for arbitrary source and target type vectors

Equations
source
def typevec.append_fun {n : ℕ} {α : typevec n} {α' : typevec n} {β : Type u_1} {β' : Type u_2} (f : α.arrow α') (g : β → β') :
(α ::: β).arrow (α' ::: β')

append an arrow and a function as well as their respective source and target types / typevecs

Equations
source
def typevec.drop_fun {n : ℕ} {α : typevec (n + 1)} {β : typevec (n + 1)} (f : α.arrow β) :
α.drop.arrow β.drop

split off the prefix of an arrow

Equations
source
def typevec.last_fun {n : ℕ} {α : typevec (n + 1)} {β : typevec (n + 1)} (f : α.arrow β) :
α.last → β.last

split off the last function of an arrow

Equations
source
def typevec.nil_fun {α : typevec 0} {β : typevec 0} :
α.arrow β

arrow in the category of 0-length vectors

Equations
source
theorem typevec.eq_of_drop_last_eq {n : ℕ} {α : typevec (n + 1)} {β : typevec (n + 1)} {f g : α.arrow β} (h₀ : typevec.drop_fun f = typevec.drop_fun g) (h₁ : typevec.last_fun f = typevec.last_fun g) :
f = g
source
@[simp]
theorem typevec.drop_fun_split_fun {n : ℕ} {α : typevec (n + 1)} {α' : typevec (n + 1)} (f : α.drop.arrow α'.drop) (g : α.last → α'.last) :
typevec.drop_fun (typevec.split_fun f g) = f
source
def typevec.arrow.mp {n : ℕ} {α β : typevec n} (h : α = β) :
α.arrow β

turn an equality into an arrow

Equations
source
def typevec.arrow.mpr {n : ℕ} {α β : typevec n} (h : α = β) :
β.arrow α

turn an equality into an arrow, with reverse direction

Equations
source
def typevec.to_append1_drop_last {n : ℕ} {α : typevec (n + 1)} :
α.arrow (α.drop ::: α.last)

decompose a vector into its prefix appended with its last element

Equations
source
def typevec.from_append1_drop_last {n : ℕ} {α : typevec (n + 1)} :
(α.drop ::: α.last).arrow α

stitch two bits of a vector back together

Equations
source
@[simp]
theorem typevec.last_fun_split_fun {n : ℕ} {α : typevec (n + 1)} {α' : typevec (n + 1)} (f : α.drop.arrow α'.drop) (g : α.last → α'.last) :
typevec.last_fun (typevec.split_fun f g) = g
source
@[simp]
theorem typevec.drop_fun_append_fun {n : ℕ} {α : typevec n} {α' : typevec n} {β : Type u_1} {β' : Type u_2} (f : α.arrow α') (g : β → β') :
typevec.drop_fun (f ::: g) = f
source
@[simp]
theorem typevec.last_fun_append_fun {n : ℕ} {α : typevec n} {α' : typevec n} {β : Type u_1} {β' : Type u_2} (f : α.arrow α') (g : β → β') :
typevec.last_fun (f ::: g) = g
source
theorem typevec.split_drop_fun_last_fun {n : ℕ} {α : typevec (n + 1)} {α' : typevec (n + 1)} (f : α.arrow α') :
typevec.split_fun (typevec.drop_fun f) (typevec.last_fun f) = f
source
theorem typevec.split_fun_inj {n : ℕ} {α : typevec (n + 1)} {α' : typevec (n + 1)} {f f' : α.drop.arrow α'.drop} {g g' : α.last → α'.last} (H : typevec.split_fun f g = typevec.split_fun f' g') :
f = f' ∧ g = g'
source
theorem typevec.append_fun_inj {n : ℕ} {α : typevec n} {α' : typevec n} {β : Type u_1} {β' : Type u_2} {f f' : α.arrow α'} {g g' : β → β'} :
f ::: g = f' ::: g' → f = f' ∧ g = g'
source
theorem typevec.split_fun_comp {n : ℕ} {α₀ : typevec (n + 1)} {α₁ : typevec (n + 1)} {α₂ : typevec (n + 1)} (f₀ : α₀.drop.arrow α₁.drop) (f₁ : α₁.drop.arrow α₂.drop) (g₀ : α₀.last → α₁.last) (g₁ : α₁.last → α₂.last) :
typevec.split_fun (typevec.comp f₁ f₀) (g₁ ∘ g₀) = typevec.comp (typevec.split_fun f₁ g₁) (typevec.split_fun f₀ g₀)
source
theorem typevec.append_fun_comp_split_fun {n : ℕ} {α : typevec n} {γ : typevec n} {β : Type u_1} {δ : Type u_2} {ε : typevec (n + 1)} (f₀ : ε.drop.arrow α) (f₁ : α.arrow γ) (g₀ : ε.last → β) (g₁ : β → δ) :
typevec.comp (f₁ ::: g₁) (typevec.split_fun f₀ g₀) = typevec.split_fun (typevec.comp f₁ f₀) (g₁ ∘ g₀)
source
theorem typevec.append_fun_comp {n : ℕ} {α₀ : typevec n} {α₁ : typevec n} {α₂ : typevec n} {β₀ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f₀ : α₀.arrow α₁) (f₁ : α₁.arrow α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) :
typevec.comp f₁ f₀ ::: g₁ ∘ g₀ = typevec.comp (f₁ ::: g₁) (f₀ ::: g₀)
source
theorem typevec.append_fun_comp' {n : ℕ} {α₀ : typevec n} {α₁ : typevec n} {α₂ : typevec n} {β₀ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f₀ : α₀.arrow α₁) (f₁ : α₁.arrow α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) :
typevec.comp (f₁ ::: g₁) (f₀ ::: g₀) = typevec.comp f₁ f₀ ::: g₁ ∘ g₀
source
theorem typevec.nil_fun_comp {α₀ : typevec 0} (f₀ : α₀.arrow fin2.elim0) :
typevec.comp typevec.nil_fun f₀ = f₀
source
theorem typevec.append_fun_comp_id {n : ℕ} {α : typevec n} {β₀ β₁ β₂ : Type u_1} (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) :
typevec.id ::: g₁ ∘ g₀ = typevec.comp (typevec.id ::: g₁) (typevec.id ::: g₀)
source
@[simp]
theorem typevec.drop_fun_comp {n : ℕ} {α₀ : typevec (n + 1)} {α₁ : typevec (n + 1)} {α₂ : typevec (n + 1)} (f₀ : α₀.arrow α₁) (f₁ : α₁.arrow α₂) :
typevec.drop_fun (typevec.comp f₁ f₀) = typevec.comp (typevec.drop_fun f₁) (typevec.drop_fun f₀)
source
@[simp]
theorem typevec.last_fun_comp {n : ℕ} {α₀ : typevec (n + 1)} {α₁ : typevec (n + 1)} {α₂ : typevec (n + 1)} (f₀ : α₀.arrow α₁) (f₁ : α₁.arrow α₂) :
typevec.last_fun (typevec.comp f₁ f₀) = typevec.last_fun f₁ ∘ typevec.last_fun f₀
source
theorem typevec.append_fun_aux {n : ℕ} {α : typevec n} {α' : typevec n} {β : Type u_1} {β' : Type u_2} (f : (α ::: β).arrow (α' ::: β')) :
typevec.drop_fun f ::: typevec.last_fun f = f
source
theorem typevec.append_fun_id_id {n : ℕ} {α : typevec n} {β : Type u_1} :
typevec.id ::: id = typevec.id
source
@[protected, instance]
def typevec.subsingleton0  :
subsingleton (typevec 0)
source
@[protected]
def typevec.cases_nil {β : typevec 0 → Sort u_2} (f : β fin2.elim0) (v : typevec 0) :
β v

cases distinction for 0-length type vector

Equations
source
@[protected]
def typevec.cases_cons (n : ℕ) {β : typevec (n + 1) → Sort u_2} (f : Π (t : Type u_1) (v : typevec n), β (v ::: t)) (v : typevec (n + 1)) :
β v

cases distinction for (n+1)-length type vector

Equations
source
@[protected]
theorem typevec.cases_nil_append1 {β : typevec 0 → Sort u_2} (f : β fin2.elim0) :
typevec.cases_nil f fin2.elim0 = f
source
@[protected]
theorem typevec.cases_cons_append1 (n : ℕ) {β : typevec (n + 1) → Sort u_2} (f : Π (t : Type u_1) (v : typevec n), β (v ::: t)) (v : typevec n) (α : Type u_1) :
typevec.cases_cons n f (v ::: α) = f α v
source
def typevec.typevec_cases_nil₃ {β : Π (v : typevec 0) (v' : typevec 0), v.arrow v' → Sort u_3} (f : β fin2.elim0 fin2.elim0 typevec.nil_fun) (v : typevec 0) (v' : typevec 0) (fs : v.arrow v') :
β v v' fs

cases distinction for an arrow in the category of 0-length type vectors

Equations
source
def typevec.typevec_cases_cons₃ (n : ℕ) {β : Π (v : typevec (n + 1)) (v' : typevec (n + 1)), v.arrow v' → Sort u_3} (F : Π (t : Type u_1) (t' : Type u_2) (f : t → t') (v : typevec n) (v' : typevec n) (fs : v.arrow v'), β (v ::: t) (v' ::: t') (fs ::: f)) (v : typevec (n + 1)) (v' : typevec (n + 1)) (fs : v.arrow v') :
β v v' fs

cases distinction for an arrow in the category of (n+1)-length type vectors

Equations
source
def typevec.typevec_cases_nil₂ {β : typevec.arrow fin2.elim0 fin2.elim0 → Sort u_3} (f : β typevec.nil_fun) (f_1 : typevec.arrow fin2.elim0 fin2.elim0) :
β f_1

specialized cases distinction for an arrow in the category of 0-length type vectors

Equations
source
def typevec.typevec_cases_cons₂ (n : ℕ) (t : Type u_1) (t' : Type u_2) (v : typevec n) (v' : typevec n) {β : (v ::: t).arrow (v' ::: t') → Sort u_3} (F : Π (f : t → t') (fs : v.arrow v'), β (fs ::: f)) (fs : (v ::: t).arrow (v' ::: t')) :
β fs

specialized cases distinction for an arrow in the category of (n+1)-length type vectors

Equations
source
theorem typevec.typevec_cases_nil₂_append_fun {β : typevec.arrow fin2.elim0 fin2.elim0 → Sort u_3} (f : β typevec.nil_fun) :
typevec.typevec_cases_nil₂ f typevec.nil_fun = f
source
theorem typevec.typevec_cases_cons₂_append_fun (n : ℕ) (t : Type u_1) (t' : Type u_2) (v : typevec n) (v' : typevec n) {β : (v ::: t).arrow (v' ::: t') → Sort u_3} (F : Π (f : t → t') (fs : v.arrow v'), β (fs ::: f)) (f : t → t') (fs : v.arrow v') :
typevec.typevec_cases_cons₂ n t t' v v' F (fs ::: f) = F f fs
source
def typevec.pred_last {n : ℕ} (α : typevec n) {β : Type u_1} (p : β → Prop) ⦃i : fin2 (n + 1)⦄ :
(α ::: β) i → Prop

pred_last α p x predicates p of the last element of x : α.append1 β.

Equations
source
def typevec.rel_last {n : ℕ} (α : typevec n) {β γ : Type u_1} (r : β → γ → Prop) ⦃i : fin2 (n + 1)⦄ :
(α ::: β) i → (α ::: γ) i → Prop

rel_last α r x y says that p the last elements of x y : α.append1 β are related by r and all the other elements are equal.

Equations
source
def typevec.repeat (n : ℕ) (t : Type u_1) :
typevec n

repeat n t is a n-length type vector that contains n occurences of t

Equations
source
def typevec.prod {n : ℕ} (α β : typevec n) :
typevec n

prod α β is the pointwise product of the components of α and β

Equations
source
@[protected]
def typevec.const {β : Type u_1} (x : β) {n : ℕ} (α : typevec n) :
α.arrow (typevec.repeat n β)

const x α is an arrow that ignores its source and constructs a typevec that contains nothing but x

Equations
source
def typevec.repeat_eq {n : ℕ} (α : typevec n) :
(α.prod α).arrow (typevec.repeat n Prop)

vector of equality on a product of vectors

Equations
source
theorem typevec.const_append1 {β : Type u_1} {γ : Type u_2} (x : γ) {n : ℕ} (α : typevec n) :
typevec.const x (α ::: β) = typevec.const x α ::: λ (_x : β), x
source
theorem typevec.eq_nil_fun {α : typevec 0} {β : typevec 0} (f : α.arrow β) :
f = typevec.nil_fun
source
theorem typevec.id_eq_nil_fun {α : typevec 0} :
typevec.id = typevec.nil_fun
source
theorem typevec.const_nil {β : Type u_1} (x : β) (α : typevec 0) :
typevec.const x α = typevec.nil_fun
source
theorem typevec.repeat_eq_append1 {β : Type u_1} {n : ℕ} (α : typevec n) :
(α ::: β).repeat_eq = typevec.split_fun α.repeat_eq (function.uncurry eq)
source
theorem typevec.repeat_eq_nil (α : typevec 0) :
α.repeat_eq = typevec.nil_fun
source
def typevec.pred_last' {n : ℕ} (α : typevec n) {β : Type u_1} (p : β → Prop) :
(α ::: β).arrow (typevec.repeat (n + 1) Prop)

predicate on a type vector to constrain only the last object

Equations
source
def typevec.rel_last' {n : ℕ} (α : typevec n) {β : Type u_1} (p : β → β → Prop) :
((α ::: β).prod (α ::: β)).arrow (typevec.repeat (n + 1) Prop)

predicate on the product of two type vectors to constrain only their last object

Equations
source
def typevec.curry {n : ℕ} (F : typevec (n + 1) → Type u_1) (α : Type u) (β : typevec n) :
Type u_1

given F : typevec.{u} (n+1) → Type u, curry F : Type u → typevec.{u} → Type u, i.e. its first argument can be fed in separately from the rest of the vector of arguments

Equations
Instances for typevec.curry
source
@[protected, instance]
def typevec.curry.inhabited {n : ℕ} (F : typevec (n + 1) → Type u_1) (α : Type u) (β : typevec n) [I : inhabited (F (β ::: α))] :
inhabited (typevec.curry F α β)
Equations
source
def typevec.drop_repeat (α : Type u_1) {n : ℕ} :
(typevec.repeat n.succ α).drop.arrow (typevec.repeat n α)

arrow to remove one element of a repeat vector

Equations
source
def typevec.of_repeat {α : Type u_1} {n : ℕ} {i : fin2 n} :
typevec.repeat n α i → α

projection for a repeat vector

Equations
source
theorem typevec.const_iff_true {n : ℕ} {α : typevec n} {i : fin2 n} {x : α i} {p : Prop} :
typevec.of_repeat (typevec.const p α i x) ↔ p
source
def typevec.prod.fst {n : ℕ} {α β : typevec n} :
(α.prod β).arrow α

left projection of a prod vector

Equations
source
def typevec.prod.snd {n : ℕ} {α β : typevec n} :
(α.prod β).arrow β

right projection of a prod vector

Equations
source
def typevec.prod.diag {n : ℕ} {α : typevec n} :
α.arrow (α.prod α)

introduce a product where both components are the same

Equations
source
def typevec.prod.mk {n : ℕ} {α β : typevec n} (i : fin2 n) :
α i → β i → α.prod β i

constructor for prod

Equations
source
@[simp]
theorem typevec.prod_fst_mk {n : ℕ} {α β : typevec n} (i : fin2 n) (a : α i) (b : β i) :
typevec.prod.fst i (typevec.prod.mk i a b) = a
source
@[simp]
theorem typevec.prod_snd_mk {n : ℕ} {α β : typevec n} (i : fin2 n) (a : α i) (b : β i) :
typevec.prod.snd i (typevec.prod.mk i a b) = b
source
@[protected]
def typevec.prod.map {n : ℕ} {α α' β β' : typevec n} :
α.arrow β → α'.arrow β' → (α.prod α').arrow (β.prod β')

prod is functorial

Equations
source
theorem typevec.fst_prod_mk {n : ℕ} {α α' β β' : typevec n} (f : α.arrow β) (g : α'.arrow β') :
typevec.comp typevec.prod.fst (typevec.prod.map f g) = typevec.comp f typevec.prod.fst
source
theorem typevec.snd_prod_mk {n : ℕ} {α α' β β' : typevec n} (f : α.arrow β) (g : α'.arrow β') :
typevec.comp typevec.prod.snd (typevec.prod.map f g) = typevec.comp g typevec.prod.snd
source
theorem typevec.fst_diag {n : ℕ} {α : typevec n} :
typevec.comp typevec.prod.fst typevec.prod.diag = typevec.id
source
theorem typevec.snd_diag {n : ℕ} {α : typevec n} :
typevec.comp typevec.prod.snd typevec.prod.diag = typevec.id
source
theorem typevec.repeat_eq_iff_eq {n : ℕ} {α : typevec n} {i : fin2 n} {x y : α i} :
typevec.of_repeat (α.repeat_eq i (typevec.prod.mk i x y)) ↔ x = y
source
def typevec.subtype_ {n : ℕ} {α : typevec n} (p : α.arrow (typevec.repeat n Prop)) :
typevec n

given a predicate vector p over vector α, subtype_ p is the type of vectors that contain an α that satisfies p

Equations
source
def typevec.subtype_val {n : ℕ} {α : typevec n} (p : α.arrow (typevec.repeat n Prop)) :
(typevec.subtype_ p).arrow α

projection on subtype_

Equations
source
def typevec.to_subtype {n : ℕ} {α : typevec n} (p : α.arrow (typevec.repeat n Prop)) :
typevec.arrow (λ (i : fin2 n), {x // typevec.of_repeat (p i x)}) (typevec.subtype_ p)

arrow that rearranges the type of subtype_ to turn a subtype of vector into a vector of subtypes

Equations
source
def typevec.of_subtype {n : ℕ} {α : typevec n} (p : α.arrow (typevec.repeat n Prop)) :
(typevec.subtype_ p).arrow (λ (i : fin2 n), {x // typevec.of_repeat (p i x)})

arrow that rearranges the type of subtype_ to turn a vector of subtypes into a subtype of vector

Equations
source
def typevec.to_subtype' {n : ℕ} {α : typevec n} (p : (α.prod α).arrow (typevec.repeat n Prop)) :
typevec.arrow (λ (i : fin2 n), {x // typevec.of_repeat (p i (typevec.prod.mk i x.fst x.snd))}) (typevec.subtype_ p)

similar to to_subtype adapted to relations (i.e. predicate on product)

Equations
source
def typevec.of_subtype' {n : ℕ} {α : typevec n} (p : (α.prod α).arrow (typevec.repeat n Prop)) :
(typevec.subtype_ p).arrow (λ (i : fin2 n), {x // typevec.of_repeat (p i (typevec.prod.mk i x.fst x.snd))})

similar to of_subtype adapted to relations (i.e. predicate on product)

Equations
source
def typevec.diag_sub {n : ℕ} {α : typevec n} :
α.arrow (typevec.subtype_ α.repeat_eq)

similar to diag but the target vector is a subtype_ guaranteeing the equality of the components

Equations
source
theorem typevec.subtype_val_nil {α : typevec 0} (ps : α.arrow (typevec.repeat 0 Prop)) :
typevec.subtype_val ps = typevec.nil_fun
source
theorem typevec.diag_sub_val {n : ℕ} {α : typevec n} :
typevec.comp (typevec.subtype_val α.repeat_eq) typevec.diag_sub = typevec.prod.diag
source
theorem typevec.prod_id {n : ℕ} {α β : typevec n} :
typevec.prod.map typevec.id typevec.id = typevec.id
source
theorem typevec.append_prod_append_fun {n : ℕ} {α α' β β' : typevec n} {φ φ' ψ ψ' : Type u} {f₀ : α.arrow α'} {g₀ : β.arrow β'} {f₁ : φ → φ'} {g₁ : ψ → ψ'} :
typevec.prod.map f₀ g₀ ::: prod.map f₁ g₁ = typevec.prod.map (f₀ ::: f₁) (g₀ ::: g₁)
source
@[simp]
theorem typevec.drop_fun_diag {n : ℕ} {α : typevec (n + 1)} :
typevec.drop_fun typevec.prod.diag = typevec.prod.diag
source
@[simp]
theorem typevec.drop_fun_subtype_val {n : ℕ} {α : typevec (n + 1)} (p : α.arrow (typevec.repeat (n + 1) Prop)) :
typevec.drop_fun (typevec.subtype_val p) = typevec.subtype_val (typevec.drop_fun p)
source
@[simp]
theorem typevec.last_fun_subtype_val {n : ℕ} {α : typevec (n + 1)} (p : α.arrow (typevec.repeat (n + 1) Prop)) :
typevec.last_fun (typevec.subtype_val p) = subtype.val
source
@[simp]
theorem typevec.drop_fun_to_subtype {n : ℕ} {α : typevec (n + 1)} (p : α.arrow (typevec.repeat (n + 1) Prop)) :
typevec.drop_fun (typevec.to_subtype p) = typevec.to_subtype (λ (i : fin2 n) (x : α i.fs), p i.fs x)
source
@[simp]
theorem typevec.last_fun_to_subtype {n : ℕ} {α : typevec (n + 1)} (p : α.arrow (typevec.repeat (n + 1) Prop)) :
typevec.last_fun (typevec.to_subtype p) = id
source
@[simp]
theorem typevec.drop_fun_of_subtype {n : ℕ} {α : typevec (n + 1)} (p : α.arrow (typevec.repeat (n + 1) Prop)) :
typevec.drop_fun (typevec.of_subtype p) = typevec.of_subtype (typevec.drop_fun p)
source
@[simp]
theorem typevec.last_fun_of_subtype {n : ℕ} {α : typevec (n + 1)} (p : α.arrow (typevec.repeat (n + 1) Prop)) :
typevec.last_fun (typevec.of_subtype p) = id
source
@[simp]
theorem typevec.drop_fun_rel_last {n : ℕ} {α : typevec n} {β : Type u_1} (R : β → β → Prop) :
typevec.drop_fun (α.rel_last' R) = α.repeat_eq
source
@[simp]
theorem typevec.drop_fun_prod {n : ℕ} {α α' β β' : typevec (n + 1)} (f : α.arrow β) (f' : α'.arrow β') :
typevec.drop_fun (typevec.prod.map f f') = typevec.prod.map (typevec.drop_fun f) (typevec.drop_fun f')
source
@[simp]
theorem typevec.last_fun_prod {n : ℕ} {α α' β β' : typevec (n + 1)} (f : α.arrow β) (f' : α'.arrow β') :
typevec.last_fun (typevec.prod.map f f') = prod.map (typevec.last_fun f) (typevec.last_fun f')
source
@[simp]
theorem typevec.drop_fun_from_append1_drop_last {n : ℕ} {α : typevec (n + 1)} :
typevec.drop_fun typevec.from_append1_drop_last = typevec.id
source
@[simp]
theorem typevec.last_fun_from_append1_drop_last {n : ℕ} {α : typevec (n + 1)} :
typevec.last_fun typevec.from_append1_drop_last = id
source
@[simp]
theorem typevec.drop_fun_id {n : ℕ} {α : typevec (n + 1)} :
typevec.drop_fun typevec.id = typevec.id
source
@[simp]
theorem typevec.prod_map_id {n : ℕ} {α β : typevec n} :
typevec.prod.map typevec.id typevec.id = typevec.id
source
@[simp]
theorem typevec.subtype_val_diag_sub {n : ℕ} {α : typevec n} :
typevec.comp (typevec.subtype_val α.repeat_eq) typevec.diag_sub = typevec.prod.diag
source
@[simp]
theorem typevec.to_subtype_of_subtype {n : ℕ} {α : typevec n} (p : α.arrow (typevec.repeat n Prop)) :
typevec.comp (typevec.to_subtype p) (typevec.of_subtype p) = typevec.id
source
@[simp]
theorem typevec.subtype_val_to_subtype {n : ℕ} {α : typevec n} (p : α.arrow (typevec.repeat n Prop)) :
typevec.comp (typevec.subtype_val p) (typevec.to_subtype p) = λ (_x : fin2 n), subtype.val
source
@[simp]
theorem typevec.to_subtype_of_subtype_assoc {n : ℕ} {α : typevec n} {β : typevec n} (p : α.arrow (typevec.repeat n Prop)) (f : β.arrow (typevec.subtype_ p)) :
typevec.comp (typevec.to_subtype p) (typevec.comp (typevec.of_subtype (λ (i : fin2 n) (x : α i), p i x)) f) = f
source
@[simp]
theorem typevec.to_subtype'_of_subtype' {n : ℕ} {α : typevec n} (r : (α.prod α).arrow (typevec.repeat n Prop)) :
typevec.comp (typevec.to_subtype' r) (typevec.of_subtype' r) = typevec.id
source
theorem typevec.subtype_val_to_subtype' {n : ℕ} {α : typevec n} (r : (α.prod α).arrow (typevec.repeat n Prop)) :
typevec.comp (typevec.subtype_val r) (typevec.to_subtype' r) = λ (i : fin2 n) (x : (λ (i : fin2 n), {x // typevec.of_repeat (r i (typevec.prod.mk i x.fst x.snd))}) i), typevec.prod.mk i x.val.fst x.val.snd