biUnion_congr_of_le — Mathlib

English

If two prepartitions π1 and π2 of a box I are equal, and the indexwise subpartitions πi1 and πi2 agree on every subbox J ≤ I, then the corresponding BiUnion constructions are equal: π1.biUnion πi1 = π2.biUnion πi2.

Русский

Если две предварительные разбиения π1 и π2 коробки I совпадают, и соответствующие подразбиения πi1 и πi2 совпадают для каждого J ≤ I, то биUnion-образования совпадают: π1.biUnion πi1 = π2.biUnion πi2.

LaTeX

$$$ (h : \\pi_1 = \\pi_2) \\rightarrow (h_i : \\forall J \\le I, \\pi_{i1} J = \\pi_{i2} J) \\rightarrow \\pi_1.biUnion \\pi_{i1} = \\pi_2.biUnion \\pi_{i2} $$$

Lean4

theorem biUnion_congr_of_le (h : π₁ = π₂) (hi : ∀ J ≤ I, πi₁ J = πi₂ J) : π₁.biUnion πi₁ = π₂.biUnion πi₂ :=
  biUnion_congr h fun J hJ => hi J (π₁.le_of_mem hJ)

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