finChoiceEquiv — Mathlib

English

Equivalence between uniform truncated choices and truncated function space.

Русский

Эквивалентность между равномерным выбором с усечением и усечённым пространством функций.

LaTeX

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

Lean4

/-- `Trunc.finChoice` as an equivalence. -/
@[simps]
def finChoiceEquiv : (∀ i, Trunc (α i)) ≃ Trunc (∀ i, α i)
    where
  toFun := finChoice
  invFun q i := q.map (· i)
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

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