piFinset_of_isEmpty

Mathlib.Data.Fintype.Pi

URI: https://scilib.ai/kg/mathlib#Fintype.piFinset_of_isEmpty

English

If the index α is empty, then piFinset s equals the universal finite set

Русский

Если индекс α пуст, то piFinset s равен универсуальному конечному множеству.

LaTeX

$$$[\\text{IsEmpty }\\alpha] \\; \\operatorname{piFinset} s = \\text{univ}.$$$

Lean4

@[simp]
theorem piFinset_of_isEmpty [IsEmpty α] (s : ∀ a, Finset (γ a)) : piFinset s = univ :=
  eq_univ_of_forall fun _ ↦ by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru