univ_pi_empty

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.univ_pi_empty

English

If the index type is nonempty, then pi univ (fun _ => ∅) = ∅.

Русский

Если индексный тип непуст, то pi по универсуму от пустого множества равен пустоте.

LaTeX

$$$ (\text{pi univ } (\lambda _, \ emptyset)) = \emptyset $$$

Lean4

@[simp]
theorem univ_pi_empty [h : Nonempty ι] : pi univ (fun _ => ∅ : ∀ i, Set (α i)) = ∅ :=
  univ_pi_eq_empty_iff.2 <| h.elim fun x => ⟨x, rfl⟩

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

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

Разделы

Аффилиация

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