finPi — Mathlib

English

For a finite index type α and a family π: α → Type*, the encodability of ∀ a ∈ α, π(a) holds (via an equivariant construction).

Русский

Для конечного множества индексов α и семейства π: α → Type* кодируемость ∀ a, π(a) достигается через соответствие.

LaTeX

$$$ [\\Encodable(\\forall a:\\, Fin\\ n, π(a))] $$$

Lean4

instance finPi (n) (π : Fin n → Type*) [∀ i, Encodable (π i)] : Encodable (∀ i, π i) :=
  ofEquiv _
    (Equiv.piEquivSubtypeSigma (Fin n) π)
      -- TODO: Unify with `fintypePi` and find a better name

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