English
The universal property over all J in π.biUnionTagged(πi) is equivalent to, for every J in π and every J' in πi J, the predicate holds for J'.
Русский
Универсальная характеристика над всеми J в π.biUnionTagged(πi) эквивалентна тому, что для каждого J в π и каждого J' в πi J выполняется свойство для J'.
LaTeX
$$$ (\\forall J \\in \\pi.biUnionTagged \\pi_i,\\; p((\\pi.biUnionTagged \\pi_i).tag J) J) \\iff\\ (\\forall J \\in \\pi,\\; \\forall J' \\in \\pi_i J,\\; p((\\pi_i J).tag J') J') $$$
Lean4
theorem forall_biUnionTagged (p : (ι → ℝ) → Box ι → Prop) (π : Prepartition I) (πi : ∀ J, TaggedPrepartition J) :
(∀ J ∈ π.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J' :=
by
simp only [mem_biUnionTagged]
refine ⟨fun H J hJ J' hJ' => ?_, fun H J' ⟨J, hJ, hJ'⟩ => ?_⟩
· rw [← π.tag_biUnionTagged hJ hJ']
exact H J' ⟨J, hJ, hJ'⟩
· rw [π.tag_biUnionTagged hJ hJ']
exact H J hJ J' hJ'
