compl_top

Mathlib.Analysis.BoxIntegral.Partition.Split

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

English

The complement of the top prepartition is the bottom prepartition.

Русский

Дополнение верхнего предразбиения равно нижнему предразбиению.

LaTeX

$$$ \\top.\\mathrm{compl} = \\bot$$$

Lean4

@[simp]
theorem compl_top : (⊤ : Prepartition I).compl = ⊥ :=
  (isPartitionTop I).compl_eq_bot

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

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

Разделы

Аффилиация

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