English
For a family of types α i with Setoid S i, and a function f : ∀ i, α i, the quotient choice of the family equals the quotient of the function: Quotient.choice (S) (f) = ⟦f⟧.
Русский
Для семейства типов α_i с множителями эквивалентности S_i и функции f: ∀ i, α_i, выбор по квотам семейства равен классу функции: Quotient.choice (S) f = ⟦f⟧.
LaTeX
$$$\\operatorname{Quotient.choice}(S)(f) = \\overline{f}$$$
Lean4
@[simp]
theorem choice_eq {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)} (f : ∀ i, α i) :
(Quotient.choice (S := S) fun i ↦ ⟦f i⟧) = ⟦f⟧ :=
Quotient.sound fun _ ↦ Quotient.mk_out _
