univ_prod_univ

Mathlib.Data.Set.Prod

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

English

The product of the universes is universal: univ × univ = univ.

Русский

Произведение универсумов есть универсум: univ × univ = univ.

LaTeX

$$$ \mathrm{univ}_{\alpha} \times \mathrm{univ}_{\beta} = \mathrm{univ}_{\alpha \times \beta} $$$

Lean4

@[simp, mfld_simps]
theorem univ_prod_univ : @univ α ×ˢ @univ β = univ := by
  ext
  exact iff_of_eq (true_and _)

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

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

Разделы

Аффилиация

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