English
A point y is in I.splitCenterBox s exactly when y is in I and, coordinatewise, (I.lower i + I.upper i)/2 < y_i iff i ∈ s.
Русский
Точка y принадлежит I.splitCenterBox s тогда и только тогда, когда y ∈ I и по каждой координате выполняется (I.lower i + I.upper i)/2 < y_i ⇔ i ∈ s.
LaTeX
$$$$y \in I.splitCenterBox s \;\iff\; y \in I \land \forall i, \frac{I.lower(i) + I.upper(i)}{2} < y_i \ \iff\ i \in s.$$$$
Lean4
theorem mem_splitCenterBox {s : Set ι} {y : ι → ℝ} :
y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ i, (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s :=
by
simp only [splitCenterBox, mem_def, ← forall_and]
refine forall_congr' fun i ↦ ?_
dsimp only [Set.piecewise]
split_ifs with hs <;> simp only [hs, iff_true, iff_false, not_lt]
exacts [⟨fun H ↦ ⟨⟨(left_lt_add_div_two.2 (I.lower_lt_upper i)).trans H.1, H.2⟩, H.1⟩, fun H ↦ ⟨H.2, H.1.2⟩⟩,
⟨fun H ↦ ⟨⟨H.1, H.2.trans (add_div_two_lt_right.2 (I.lower_lt_upper i)).le⟩, H.2⟩, fun H ↦ ⟨H.1.1, H.2⟩⟩]
