piFinset_eq_empty

Mathlib.Data.Fintype.Pi

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

English

The piFinset is empty exactly when at least one coordinate family s(i) is empty.

Русский

piFinset пуст тогда, когда хотя бы одно семейство координат s(i) пусто.

LaTeX

$$$\\operatorname{piFinset} s = \\varnothing \\quad\\Longleftrightarrow\\quad \\exists i,\\ s(i) = \\varnothing.$$$

Lean4

@[simp]
theorem piFinset_eq_empty : piFinset s = ∅ ↔ ∃ i, s i = ∅ := by simp [piFinset]

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

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

Разделы

Аффилиация

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