tag_biUnionTagged — Mathlib

English

The tag of a box J' in the biUnionTagged equals the tag of the corresponding J in π.

Русский

Метка коробки J' в biUnionTagged равна метке соответствующей коробки J в π.

LaTeX

$$$ (\\pi.biUnionTagged \\pi_i).tag(J') = (\\pi_i(J)).tag(J') $$$

Lean4

theorem tag_biUnionTagged (π : Prepartition I) {πi : ∀ J, TaggedPrepartition J} (hJ : J ∈ π) {J'} (hJ' : J' ∈ πi J) :
    (π.biUnionTagged πi).tag J' = (πi J).tag J' :=
  by
  rw [← π.biUnionIndex_of_mem (πi := fun J => (πi J).toPrepartition) hJ hJ']
  rfl

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