univ_pi_univ — Mathlib

English

The universal piFinset over univ at each index equals the univ over the function space.

Русский

Универсальный пи-финсет над унивом по каждой координате равен униву над пространством функций.

LaTeX

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

Lean4

@[simp]
theorem univ_pi_univ {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α] [∀ a, Fintype (β a)] :
    (Finset.univ.pi fun a : α => (Finset.univ : Finset (β a))) = Finset.univ := by ext; simp

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