univ_sigma_preimage_mk

Mathlib.Data.Set.Sigma

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

English

The sigma of univ with preimages of a set under Sigma.mk equals the set itself.

Русский

Сигма от универсума с предобразами Sigma.mk равна самому множеству.

LaTeX

$$$\\mathrm{univ}.\\sigma (\\lambda i. \\mathrm{preimage}(\\mathrm{Sigma.mk} i)\\, s) = s$$$

Lean4

@[simp]
theorem univ_sigma_preimage_mk (s : Set (Σ i, α i)) : (univ : Set ι).sigma (fun i ↦ Sigma.mk i ⁻¹' s) = s := by grind

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

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

Разделы

Аффилиация

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