tag

Mathlib.Analysis.BoxIntegral.UnitPartition

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

English

The tag of the index ν is (ν i + 1)/n for each coordinate i.

Русский

Метка индекса ν равна (ν_i + 1)/n по каждой координате i.

LaTeX

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

Lean4

/-- The tag of (the index of) a `unitPartition.box`. -/
abbrev tag (ν : ι → ℤ) : ι → ℝ := fun i ↦ (ν i + 1) / n

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

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

Разделы

Аффилиация

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