piDiag_subset_piFinset

Mathlib.Data.Fintype.Pi

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

English

The diagonal of a finite set is contained in the corresponding piFinset.

Русский

Диагональ конечного множества содержится в соответствующем piFinset.

LaTeX

$$$s.PI diag ι \\subseteq Fintype.piFinset(\\lambda x. s)$$$

Lean4

theorem piDiag_subset_piFinset [DecidableEq ι] [Fintype ι] : s.piDiag ι ⊆ Fintype.piFinset fun _ ↦ s := by
  simp [← piFinset_filter_const]

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

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

Разделы

Аффилиация

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