box_upper

Mathlib.Analysis.BoxIntegral.UnitPartition

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

English

The i-th coordinate of the upper corner of box(n,ν) equals (ν_i+1)/n.

Русский

i-й координате верхней грани коробки box(n,ν) соответствует (ν_i+1)/n.

LaTeX

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

Lean4

@[simp]
theorem box_upper [NeZero n] (ν : ι → ℤ) : (box n ν).upper = fun i ↦ ((ν i + 1) / n : ℝ) :=
  rfl

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

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

Разделы

Аффилиация

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