English
Auxiliary definition showing how to lift an existential to a truncation of a dependent sigma-type Σ' a, P a.
Русский
Вспомогательное определение, показывающее как перейти от существования ∃ a, P a к усечённому зависимому сумме Σ' a, P a.
LaTeX
$$$$ \\text{truncSigmaOfExists} \\{α\\} [Fintype α] {P : α \\to Prop} \\; (h : \\exists a, P a) : Trunc (Σ' a, P a). $$$$
Lean4
/-- Auxiliary definition to show `exists_seq_of_forall_finset_exists`. -/
noncomputable def seqOfForallFinsetExistsAux {α : Type*} [DecidableEq α] (P : α → Prop) (r : α → α → Prop)
(h : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y) : ℕ → α
| n =>
Classical.choose
(h (Finset.image (fun i : Fin n => seqOfForallFinsetExistsAux P r h i) (Finset.univ : Finset (Fin n))))
