instFintype — Mathlib

English

The piFinset over a family that is constantly univ equals the universal finite set of all functions.

Русский

piFinset, где на каждом индексе задано полное множество, совпадает с полным множеством всех функций.

LaTeX

$$$\\operatorname{piFinset}(\\lambda a. \\operatorname{univ}) = \\operatorname{univ}.$$$

Lean4

/-- A dependent product of fintypes, indexed by a fintype, is a fintype. -/
instance instFintype {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α] [∀ a, Fintype (β a)] :
    Fintype (∀ a, β a) :=
  ⟨Fintype.piFinset fun _ => univ, by simp⟩

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