box_index_tag_eq_self — Mathlib

English

If I is a box appearing in the prepartition boxes, then applying the index map to the tag of I yields the original I when reboxing with n.

Русский

Для любого I ∈ prepartition n B.boxes выполняется, что box n (index n ((prepartition n B).tag I)) = I.

LaTeX

$$$$ box\, n\bigl(\mathrm{index}\, n\bigl((\mathrm{prepartition}\, n\ B).\mathrm{tag}\\ I)\bigr) = I \quad\text{where } I \in (\mathrm{prepartition}\, n\ B).boxes.$$$$

Lean4

theorem box_index_tag_eq_self {B I : Box ι} (hI : I ∈ (prepartition n B).boxes) :
    box n (index n ((prepartition n B).tag I)) = I :=
  by
  obtain ⟨ν, hν, rfl⟩ := mem_prepartition_boxes_iff.mp hI
  rw [prepartition_tag n hν, index_tag]

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