English
Let n be a positive integer, B a box on ι, and ν a ℤ-valued index which lies in the admissibleIndex set for B. Then the tag of the box box n ν inside the unit partition coincides with the global tag, i.e. the prepartition's local tag equals the global tag.
Русский
Пусть n — положительное число, B — коробка над индексами ι, и ν — целочисленный индекс, принадлежащий допустимому множеству admissibleIndex n B. Тогда локальная метка элемента разбиения равна глобальной метке: тег разбиения (prepartition n B) для box n ν совпадает с тегом n ν.
LaTeX
$$$$(prepartition n B).tag(\mathrm{box} \, n\, \nu) = \mathrm{tag}\, n\, \nu,$$ при условии $\nu \in admissibleIndex\ n\ B$.$$
Lean4
theorem prepartition_tag {ν : ι → ℤ} {B : Box ι} (hν : ν ∈ admissibleIndex n B) :
(prepartition n B).tag (box n ν) = tag n ν :=
by
dsimp only [prepartition]
have h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν' := ⟨ν, hν, rfl⟩
rw [dif_pos h, (tag_injective n).eq_iff, ← (box_injective n).eq_iff]
exact h.choose_spec.2.symm
