sigma_eq_biUnion

Mathlib.Data.Set.Sigma

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

English

The same biUnion identity for sigma: s.sigma t equals the union over i in s of Sigma.mk i '' t i.

Русский

Та же биобъединение сигмы: s.sigma t равно объединению по i в s ∶ Sigma.mk i '' t i.

LaTeX

$$$ s \\sigma t = \\bigcup_{i \\in s} (\\Sigma\\!{\\!i}'' t(i)) $$$

Lean4

theorem sigma_eq_biUnion : s.sigma t = ⋃ i ∈ s, Sigma.mk i '' t i := by aesop

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

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

Разделы

Аффилиация

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