map_le_of_mem_box — Mathlib

English

If x ∈ box(n,d), then map(2d−1) x ≤ ∑ i (d−1) (2d−1)^i over i ∈ Fin n.

Русский

Если x ∈ box(n,d), то map(2d−1) x не превосходит сумму ∑_i (d−1) (2d−1)^i.

LaTeX

$$$ x \\in box\\, n\\, d \\Rightarrow map(2\\,d-1)\\, x \\le \\sum_{i\\in Fin\\, n} (d-1) (2\\,d-1)^{i} $$$

Lean4

theorem map_le_of_mem_box (hx : x ∈ box n d) : map (2 * d - 1) x ≤ ∑ i : Fin n, (d - 1) * (2 * d - 1) ^ (i : ℕ) :=
  map_monotone (2 * d - 1) fun _ => Nat.le_sub_one_of_lt <| mem_box.1 hx _

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