English
Let π be a prepartition of I and πi a family of prepartitions indexed by boxes J. For any π′, π′ ≤ π.biUnion πi holds if and only if π′ ≤ π and for every J ∈ π the restriction π′|J is ≤ πi(J).
Русский
Пусть π — предразбиение множества I, а πi — семейство предразбиений, индексируемое поBox J. Для любого π′ выполняется: π′ ≤ π.biUnion πi тогда и только тогда, когда π′ ≤ π и для каждого J ∈ π ограничение π′ на J удовлетворяет π′|J ≤ πi(J).
LaTeX
$$$ \pi' \le \operatorname{biUnion}(\pi, \pi_i) \;\iff\; (\pi' \le \pi) \land (\forall J \in \pi, \; \pi'.\restrict J \le \pi_i J). $$$
Lean4
theorem le_biUnion_iff {πi : ∀ J, Prepartition J} {π' : Prepartition I} :
π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J :=
by
refine ⟨fun H => ⟨H.trans (π.biUnion_le πi), fun J hJ => ?_⟩, ?_⟩
· rw [← π.restrict_biUnion πi hJ]
exact restrict_mono H
· rintro ⟨H, Hi⟩ J' hJ'
rcases H hJ' with ⟨J, hJ, hle⟩
have : J' ∈ π'.restrict J := π'.mem_restrict.2 ⟨J', hJ', (inf_of_le_right <| WithBot.coe_le_coe.2 hle).symm⟩
rcases Hi J hJ this with ⟨Ji, hJi, hlei⟩
exact ⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hlei⟩
