instSigma — Mathlib

English

If α is finite and β a finite family, then the dependent sum PSigma α β is finite.

Русский

Если α конечен и β — конечная семейство множеств, то зависимая сумма PSigma α β конечна.

LaTeX

$$$ [Finite α] \Rightarrow [\forall a, Finite (β a)] \Rightarrow Finite (Σ' a, β a) $$$

Lean4

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

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