English
If a finite hyperplane set s contains all faces of J and Js ∈ splitMany I s with J and Js non-disjoint, then Js ≤ J.
Русский
Если множество гиперплоскостей s содержит все грани J и Js ∈ splitMany I s и J, Js непересекаются, то Js ⊑ J.
LaTeX
$$$\\big(\\forall i, \\{(i,J.lower i),(i,J.upper i)\\} \\subseteq s\\big) \\\\rightarrow (Js \\in splitMany\\ I\\ s) \\rightarrow \\neg\\operatorname{Disjoint} (J, Js) \\rightarrow Js \\le J$$$
Lean4
/-- Let `s : Finset (ι × ℝ)` be a set of hyperplanes `{x : ι → ℝ | x i = r}` in `ι → ℝ` encoded as
pairs `(i, r)`. Suppose that this set contains all faces of a box `J`. The hyperplanes of `s` split
a box `I` into subboxes. Let `Js` be one of them. If `J` and `Js` have nonempty intersection, then
`Js` is a subbox of `J`. -/
theorem not_disjoint_imp_le_of_subset_of_mem_splitMany {I J Js : Box ι} {s : Finset (ι × ℝ)}
(H : ∀ i, {(i, J.lower i), (i, J.upper i)} ⊆ s) (HJs : Js ∈ splitMany I s)
(Hn : ¬Disjoint (J : WithBot (Box ι)) Js) : Js ≤ J :=
by
simp only [Finset.insert_subset_iff, Finset.singleton_subset_iff] at H
rcases Box.not_disjoint_coe_iff_nonempty_inter.mp Hn with ⟨x, hx, hxs⟩
refine fun y hy i => ⟨?_, ?_⟩
· rcases splitMany_le_split I (H i).1 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.lower i), Hle⟩
have := Hle hxs
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_lt_mem Hmem this (hx i).1] at Hle
exact (Hle hy).2
· rcases splitMany_le_split I (H i).2 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.upper i), Hle⟩
have := Hle hxs
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle
exact (Hle hy).2
