index_tag

Mathlib.Analysis.BoxIntegral.UnitPartition

URI: https://scilib.ai/kg/mathlib#BoxIntegral.unitPartition.index_tag

English

The map ν ↦ box(n,ν) is injective; different ν give different boxes.

Русский

Разбиение единичной партии отображает разные ν в разные коробки.

LaTeX

$$Injective: box(n,ν) is unique to ν.$$

Lean4

@[simp]
theorem index_tag (ν : ι → ℤ) : index n (tag n ν) = ν :=
  mem_box_iff_index.mp (tag_mem n ν)

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

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

Разделы

Аффилиация

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