union_pi

Mathlib.Data.Set.Prod

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

English

The pi-set over a union of index sets equals the intersection of the pi-sets over each piece.

Русский

Произведение по объединению индексов равно пересечению проиведения по каждому из множителей.

LaTeX

$$$ (s_1 \cup s_2).\pi t = s_1.\pi t \cap s_2.\pi t $$$

Lean4

theorem union_pi : (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t := by simp [pi, or_imp, forall_and, setOf_and]

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

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

Разделы

Аффилиация

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