English
Let α(i) be a family of preordered types indexed by Fin(n+1). For x ∈ α(0), q : ∀ i, α(i), and p : ∀ i ∈ Fin n, α(i.succ), we have cons x p ≤ q if and only if x ≤ q(0) and p ≤ tail(q).
Русский
Пусть α(i) задаёт family предикатов порядка, индексируемых по Fin(n+1). Пусть x ∈ α(0), q : ∀ i, α(i), и p : ∀ i ∈ Fin n, α(i.succ). Тогда последовательность, полученная конструктором cons x p, удовлетворяет неравенству по покомпонентному порядку: cons x p ≤ q тогда и только если x ≤ q(0) и p ≤ tail(q).
LaTeX
$$$\\text{cons } x p \\le q \\iff x \\le q_0 \\land p \\le \\text{tail}(q).$$$
Lean4
theorem cons_le [∀ i, Preorder (α i)] {x : α 0} {q : ∀ i, α i} {p : ∀ i : Fin n, α i.succ} :
cons x p ≤ q ↔ x ≤ q 0 ∧ p ≤ tail q :=
@le_cons _ (fun i ↦ (α i)ᵒᵈ) _ x q p
