iUnion_compl

Mathlib.Analysis.BoxIntegral.Partition.Split

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

English

Same as iUnion_compl: the iUnion of the complement partition equals the set difference I \\ π.iUnion.

Русский

То же, что и iUnion_compl: iUnion дополнения разбиения равно разности I \\ π.iUnion.

LaTeX

$$$\\pi.compl.\\mathrm{iUnion} = \\uparrow I \\setminus \\pi.\\mathrm{iUnion}$$$

Lean4

@[simp]
theorem iUnion_compl (π : Prepartition I) : π.compl.iUnion = ↑I \ π.iUnion :=
  π.exists_iUnion_eq_diff.choose_spec

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

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

Разделы

Аффилиация

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