liftFun_vecCons

theorem liftFun_vecCons : ∀ {α : Type u_1} {n : ℕ} (r : α → α → Prop) [inst : IsTrans α r] {f : Fin (n + 1) → α} {a : α}, ((fun x x_1 => x < x_1) ⇒ r) (Matrix.vecCons a f) (Matrix.vecCons a f) ↔ r a (f 0) ∧ ((fun x x_1 => x < x_1) ⇒ r) f f

This theorem, `liftFun_vecCons`, states that for any type `α`, natural number `n`, a relation `r` on `α` that is transitive, a function `f` from `Fin(n + 1)` to `α` and a value `a` of type `α`, the relation `r` holds between the first elements of two `vecCons` operations and the rest of the elements in them if and only if the relation `r` holds between `a` and `f(0)`, and the relation `r` holds between every pair of elements in `f` where the first element is less than the second. Here, `vecCons` is a function that prepends an element to a list, `Fin(n + 1)` is a finite set of size `n + 1`, and `r` is a binary relation on `α`. The `<` symbol denotes the natural ordering of these elements. The transitivity of `r` implies that if `r` holds between `a` and `b`, and between `b` and `c`, then `r` also holds between `a` and `c`.

More concisely: For any type `α`, natural number `n`, transitive relation `r` on `α`, function `f` from `Fin(n + 1)` to `α`, and values `a, x, y` of type `α` with `x` less than `y` in `Fin(n + 1)`, the relation `r` holds between the first elements of `vecCons a (vecCons x (f x))` and `vecCons x (vecCons a f (x + 1))` if and only if `r` holds between `a` and `f(0)` and `r` holds between every pair `(f i, f (i + 1))` for `i` less than `x`.