finChoice_eq — Mathlib

English

FinChoice acts as an equivalence between families of truncations and truncation of functions.

Русский

FinChoice действует как эквивалент между семействами усечений и усечением функций.

LaTeX

$$$\\operatorname{FinChoiceEquiv} : (\\forall i, \\operatorname{Trunc}(\\alpha i)) \\simeq \\operatorname{Trunc}(\\forall i, \\alpha i)$$$

Lean4

theorem finChoice_eq (f : ∀ i, α i) : (Trunc.finChoice fun i => Trunc.mk (f i)) = Trunc.mk f :=
  Subsingleton.elim _ _

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