English
If a1 relates to a2 by r, and each tail maps f1 i hi relates to f2 i hi by r, then the Pi-consed functions also relate: r holds pointwise after cons.
Русский
Если a1 связан с a2 отношением r, и каждый элемент хвоста удовлетворяет relation между f1 и f2, тогда конструированные через PiCons функции также связаны отношением r по всем индексам.
LaTeX
$$$\forall j \; hj,\; r (\text{cons } i l a_1 f_1 j hj) (\text{cons } i l a_2 f_2 j hj)$$$
Lean4
theorem forall_rel_cons_ext {r : ∀ ⦃i⦄, α i → α i → Prop} {a₁ a₂ : α i} {f₁ f₂ : ∀ j ∈ l, α j} (ha : r a₁ a₂)
(hf : ∀ (i : ι) (hi : i ∈ l), r (f₁ i hi) (f₂ i hi)) : ∀ j hj, r (cons _ _ a₁ f₁ j hj) (cons _ _ a₂ f₂ j hj) :=
Multiset.Pi.forall_rel_cons_ext (α := ι) (m := l) ha hf
