piFinset_univ — Mathlib

English

Same as the previous, showing consistency of piFinset with universal families.

Русский

То же самое как и ранее, демонстрируя согласованность piFinset с универсальными семействами.

LaTeX

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

Lean4

@[simp]
theorem piFinset_univ {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α] [∀ a, Fintype (β a)] :
    (Fintype.piFinset fun a : α => (Finset.univ : Finset (β a))) = (Finset.univ : Finset (∀ a, β a)) :=
  rfl

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