box_lower

Mathlib.Analysis.BoxIntegral.UnitPartition

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

English

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

Русский

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

LaTeX

$$$ (\text{box}(n,\nu)).\text{lower}_i = \frac{\nu_i}{n} \quad \forall i $$$

Lean4

@[simp]
theorem box_lower [NeZero n] (ν : ι → ℤ) : (box n ν).lower = fun i ↦ (ν i / n : ℝ) :=
  rfl

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

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

Разделы

Аффилиация

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