box — Mathlib

English

A Box constructed from a positive integer n and ν: ι → ℤ has lower ν_i/n and upper (ν_i+1)/n for each coordinate.

Русский

Коробка, заданная через n и ν: ι → ℤ, имеет нижнюю грань ν_i/n и верхнюю ν_i+1/n по каждой координате.

LaTeX

$$$\text{box}(n,\nu) \text{ has lower } = (\nu_i/n)_i \text{ and upper } = ((\nu_i+1)/n)_i$$$

Lean4

/-- A `BoxIntegral`, indexed by a positive integer `n` and `ν : ι → ℤ`, with corners `ν i / n`
and of side length `1 / n`. -/
def box [NeZero n] (ν : ι → ℤ) : Box ι where
  lower := fun i ↦ ν i / n
  upper := fun i ↦ (ν i + 1) / n
  lower_lt_upper := fun _ ↦ by simp [add_div, n.pos_of_neZero]

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