iUnion_disjUnion

Mathlib.Analysis.BoxIntegral.Partition.Tagged

URI: https://scilib.ai/kg/mathlib#BoxIntegral.TaggedPrepartition.iUnion_disjUnion

← MathLib Explorer

English

The iUnion of the disjoint union equals the union of iUnions.

Русский

Объединение iUnion дизъюнкции равно объединению iUnions.

LaTeX

$$$ (π_1.disjUnion π_2 h).iUnion = π_1.iUnion ∪ π_2.iUnion $$$

Lean4

@[simp]
theorem iUnion_disjUnion (h : Disjoint π₁.iUnion π₂.iUnion) : (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion :=
  Prepartition.iUnion_disjUnion h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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