univ_sigma_univ

Mathlib.Data.Set.Sigma

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

English

Proof sketch that the universal sigma equals the universal set.

Русский

Эскиз доказательства того, что универсальная сигма равна универсальному множеству.

LaTeX

$$Proof sketch notationally: equality follows from basic mem and ext lemmas.$$

Lean4

theorem univ_sigma_univ : (@univ ι).sigma (fun _ ↦ @univ (α i)) = univ := by grind

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

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

Разделы

Аффилиация

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