English
LiftFun translates relational statements between sequences by applying a base relation r to the first coordinate and recursively to the tail; for vecCons a f the relation reduces to r(a, f(0)) and the tail relation on f.
Русский
LiftFun переводит реляционные утверждения между последовательностями через применение базовой редукции r к первой координате и затем к хвостовой части; для vecCons a f отношение делится на r(a, f(0)) и хвостовое отношение к f.
LaTeX
$$$((\cdot < \cdot) \Rightarrow r) (\text{vecCons } a f) (\text{vecCons } a f) \iff r(a, f(0)) \land ((\cdot < \cdot) \Rightarrow r) f f.$$$
Lean4
theorem liftFun_vecCons {n : ℕ} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} {a : α} :
((· < ·) ⇒ r) (vecCons a f) (vecCons a f) ↔ r a (f 0) ∧ ((· < ·) ⇒ r) f f := by
simp only [liftFun_iff_succ r, forall_iff_succ, cons_val_succ, cons_val_zero, ← succ_castSucc, castSucc_zero]
