iUnion_single

Mathlib.Analysis.BoxIntegral.Partition.Basic

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

English

The iUnion of the top prepartition equals the whole box I.

Русский

Объединение iUnion верхнего предразбиения равно всей коробке I.

LaTeX

$$(\top : Prepartition I).iUnion = I$$

Lean4

@[simp]
theorem iUnion_single (h : J ≤ I) : (single I J h).iUnion = J := by simp [iUnion_def]

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

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

Разделы

Аффилиация

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