forall_iff_forall_tuple — Mathlib

English

For every property P on lists, P holds for all lists iff P holds for all Fuin tuples represented as List.ofFn f for some n.

Русский

Для каждого свойства P над списками выполняется, что P истинно для всех списков тогда и только тогда, когда P истинно для всех представлений в List.ofFn f для некоторого n.

LaTeX

$$$ \\forall P,\\ (\\forall l:\\ List\\ α, P\\ l) \\iff \\forall n\\ (f: Fin\\ n \\to α),\\ P(\\operatorname{List.ofFn} f) $$$

Lean4

theorem forall_iff_forall_tuple {P : List α → Prop} : (∀ l : List α, P l) ↔ ∀ (n) (f : Fin n → α), P (List.ofFn f) :=
  equivSigmaTuple.symm.surjective.forall.trans Sigma.forall

Похожие утверждения