English
The Pairwise property of the list List.ofFn f with respect to R is equivalent to R holding pairwise for all f i; i < j.
Русский
Свойство пары в списке List.ofFn f относительно R эквивалентно тому, что R выполняется для всех пар i<j.
LaTeX
$$$ (\\operatorname{List}.Pairwise\\ R\\ (\\operatorname{List.ofFn} f)) \\iff \\forall \\{i j\\}, i < j \\rightarrow R(f i)(f j) $$$
Lean4
@[simp]
theorem pairwise_ofFn {R : α → α → Prop} {n} {f : Fin n → α} : (ofFn f).Pairwise R ↔ ∀ ⦃i j⦄, i < j → R (f i) (f j) :=
by
simp only [pairwise_iff_getElem, length_ofFn, List.getElem_ofFn, Fin.forall_iff, Fin.mk_lt_mk,
forall_comm (α := (_ : Prop)) (β := ℕ)]
