iUnion_restrict

Mathlib.Analysis.BoxIntegral.Partition.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.iUnion_restrict

English

Simplified version of iUnion_restrict capturing simplified set-theoretic identities.

Русский

Упрощение iUnion_restrict иллюстрирует упрощённые преобразования множеств.

LaTeX

$$$ \\text{Set.iUnion}\\,\\bigl( \\lambda J, S(J) \\bigr) = \\ldots $$$

Lean4

@[simp]
theorem iUnion_restrict : (π.restrict J).iUnion = (J : Set (ι → ℝ)) ∩ (π.iUnion) := by
  simp [restrict, ← inter_iUnion, ← iUnion_def]

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

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

Разделы

Аффилиация

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