English
When α is finite and each π(a) is encodable, the dependent function space ∀ a, π(a) is encodable up to truncation.
Русский
Если α конечен и для каждого a выполняется, что π(a) кодируемо, то зависимая функция ∀ a, π(a) кодируема с усечением.
LaTeX
$$$ \\text{Trunc}(\\text{Encodable}(\\forall a:\\, α, \\pi(a))). $$$
Lean4
/-- When `α` is finite and all `π a` are encodable, `Π a, π a` is encodable too. Because the
encoding is not unique, we wrap it in `Trunc` to preserve computability. -/
def fintypePi (α : Type*) (π : α → Type*) [DecidableEq α] [Fintype α] [∀ a, Encodable (π a)] :
Trunc (Encodable (∀ a, π a)) :=
(Fintype.truncEncodable α).bind fun a =>
(@fintypeArrow α (Σ a, π a) _ _ (@Sigma.encodable _ _ a _)).bind fun f =>
Trunc.mk <| @Encodable.ofEquiv _ _ (@Subtype.encodable _ _ f _) (Equiv.piEquivSubtypeSigma α π)
