tag_apply

Mathlib.Analysis.BoxIntegral.UnitPartition

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

English

The value of the tag function at ν and i is (ν_i + 1)/n.

Русский

Значение функции метки в ν и координате i равно (ν_i + 1)/n.

LaTeX

$$$\text{tag}(n,\nu)_i = \dfrac{\nu_i + 1}{n}$$$

Lean4

@[simp]
theorem tag_apply (ν : ι → ℤ) (i : ι) : tag n ν i = (ν i + 1) / n :=
  rfl

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

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

Разделы

Аффилиация

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