English
If for every finite subset s of α there exists a witness y with P y and r x y for all x ∈ s, then there exists a sequence f : ℕ → α with all P-values and with r(f m, f n) for m < n.
Русский
Если для любой конечной подмножества s ⊆ α существует свидетель y с P y и r x y для всех x ∈ s, то существует последовательность f: ℕ → α такая, что все P (f n) истинны и r(f m, f n) при m < n.
LaTeX
$$$$ \\text{If } \\forall s \\subseteq_{fin} α, (\\forall x \\in s, P x) \\to \\exists y, P y \\wedge \\forall x \\in s, r x y, \\text{ then } \\exists f: \\mathbb{N} \\to α, (\\forall n, P (f n)) \\wedge \\forall m n, m < n \\to r (f m) (f n). $$$$
Lean4
/-- By iterating over the elements of a fintype, we can lift an existential statement `∃ a, P a`
to `Trunc (Σ' a, P a)`, containing data.
-/
def truncSigmaOfExists {α} [Fintype α] {P : α → Prop} [DecidablePred P] (h : ∃ a, P a) : Trunc (Σ' a, P a) :=
@truncOfNonemptyFintype (Σ' a, P a) ((Exists.elim h) fun a ha => ⟨⟨a, ha⟩⟩) _
