index_apply

Mathlib.Analysis.BoxIntegral.UnitPartition

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

English

The index at the unit partition satisfies index(n, x) = ⌈n * x_i⌉ − 1 for coordinate i.

Русский

Индекс единичного разбиения удовлетворяет index(n,x)_i = ⌈n * x_i⌉ − 1.

LaTeX

$$$index(n, x)_i = \lceil n \cdot x_i \rceil - 1$$$

Lean4

@[simp]
theorem index_apply (m : ℕ) {x : ι → ℝ} (i : ι) : index m x i = ⌈m * x i⌉ - 1 :=
  rfl

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

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

Разделы

Аффилиация

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