card_piDiag

Mathlib.Data.Finset.Pi

URI: https://scilib.ai/kg/mathlib#Finset.card_piDiag

← MathLib Explorer

English

Pi over an empty Finset is the singleton containing the empty function.

Русский

Pi над пустым Finset является синглетоном, содержащим пустую функцию.

LaTeX

$$$ pi(\\emptyset, t) = \\{ \\text{empty function} \\}$$$

Lean4

@[simp]
theorem card_piDiag (s : Finset α) (ι : Type*) [DecidableEq (ι → α)] [Nonempty ι] : (s.piDiag ι).card = s.card := by
  rw [piDiag, card_image_of_injective _ const_injective]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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