listChoice — Mathlib

Lean4
/-- Given a collection of setoids indexed by a type `ι`, a list `l` of indices, and a function that
  for each `i ∈ l` gives a term of the corresponding quotient type, then there is a corresponding
  term in the quotient of the product of the setoids indexed by `l`. -/
def listChoice {l : List ι} (q : ∀ i ∈ l, Quotient (S i)) : @Quotient (∀ i ∈ l, α i) piSetoid :=
  match l with
  | [] => ⟦nofun⟧
  | i :: _ =>
    Quotient.liftOn₂ (List.Pi.head (i := i) q) (listChoice (List.Pi.tail q)) (⟦List.Pi.cons _ _ · ·⟧)
      (fun _ _ _ _ ha hl ↦ Quotient.sound (List.Pi.forall_rel_cons_ext ha hl))
Похожие утверждения