English
There exists a finite t0 such that for all t ⊇ t0, and for all I,J ∈ Box, J' ∈ splitMany I t, if J and J' are not disjoint, then J' ≤ J.
Русский
Существует конечное t0, такое что для всех t ⊇ t0, для любых I,J, J' ∈ splitMany I t, если J и J' не непересекаются, то J' ≤ J.
LaTeX
$$$\\exists t_0, \\forall t \\supseteq t_0, \\forall I,J, J' : Box,\\ J' \\in splitMany I t \\rightarrow \\lnot Disjoint (J, J') \\rightarrow J' \\le J$$$
Lean4
/-- Let `s` be a finite set of boxes in `ℝⁿ = ι → ℝ`. Then there exists a finite set `t₀` of
hyperplanes (namely, the set of all hyperfaces of boxes in `s`) such that for any `t ⊇ t₀`
and any box `I` in `ℝⁿ` the following holds. The hyperplanes from `t` split `I` into subboxes.
Let `J'` be one of them, and let `J` be one of the boxes in `s`. If these boxes have a nonempty
intersection, then `J' ≤ J`. -/
theorem eventually_not_disjoint_imp_le_of_mem_splitMany (s : Finset (Box ι)) :
∀ᶠ t : Finset (ι × ℝ) in atTop,
∀ (I : Box ι), ∀ J ∈ s, ∀ J' ∈ splitMany I t, ¬Disjoint (J : WithBot (Box ι)) J' → J' ≤ J :=
by
classical
cases nonempty_fintype ι
refine
eventually_atTop.2
⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)}, fun t ht I J hJ J' hJ' =>
not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => ?_) hJ'⟩
exact fun p hp => ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)
