Mathlib.Data.Finite.Sigma

Module docstring

{"# Finiteness of sigma types "}

Finite.instSigma instance

{β : α → Type*} [Finite α] [∀ a, Finite (β a)] : Finite (Σ a, β a)

Full source

instance {β : α → Type*} [Finite α] [∀ a, Finite (β a)] : Finite (Σa, β a) := by
  letI := Fintype.ofFinite α
  letI := fun a => Fintype.ofFinite (β a)
  infer_instance

Finiteness of Dependent Sum Types

Informal description

For any type $\alpha$ and a family of types $\beta : \alpha \to \text{Type*}$, if $\alpha$ is finite and each $\beta(a)$ is finite for all $a \in \alpha$, then the dependent sum type $\Sigma a, \beta a$ is finite.

Finite.instPSigma instance

{ι : Sort*} {π : ι → Sort*} [Finite ι] [∀ i, Finite (π i)] : Finite (Σ' i, π i)

Full source

instance {ι : Sort*} {π : ι → Sort*} [Finite ι] [∀ i, Finite (π i)] : Finite (Σ'i, π i) :=
  of_equiv _ (Equiv.psigmaEquivSigmaPLift π).symm

Finiteness of Dependent Pair Types (`PSigma`)

Informal description

For any finite type $\iota$ and a family of types $\pi : \iota \to \text{Sort}^*$ such that each $\pi(i)$ is finite, the dependent pair type $\Sigma' i, \pi i$ (a `PSigma` type) is also finite.