mem_box_iff_index — Mathlib

English

The map index applied to tag(n,ν) returns ν; i.e., index n (tag n ν) = ν.

Русский

Указатель индекса применяется к тегу возвращает ν; то есть index n (tag n ν) = ν.

LaTeX

$$$index(n, (\text{tag}(n,\nu))) = \nu$$$

Lean4

theorem mem_box_iff_index {x : ι → ℝ} {ν : ι → ℤ} : x ∈ box n ν ↔ index n x = ν := by
  simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one,
    add_sub_cancel_right]

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