exists_iff_exists_tuple — Mathlib

English

There is a bijection between existentially quantified lists and tuples: Exists l : List α, P l ⇔ Exists n, ∃ f : Fin n → α, P (List.ofFn f).

Русский

Существование списка и кортежа эквивалентны: Exists l : List α, P l ⟺ Exists n, ∃ f : Fin n → α, P (List.ofFn f).

LaTeX

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

Lean4

theorem exists_iff_exists_tuple {P : List α → Prop} :
    (∃ l : List α, P l) ↔ ∃ (n : _) (f : Fin n → α), P (List.ofFn f) :=
  equivSigmaTuple.symm.surjective.exists.trans Sigma.exists

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