English
If a set s ⊆ ι → ℝ is bounded, then there exists a box with integral vertices that contains s.
Русский
Если множество s ⊆ ι → ℝ ограничено, существует коробка с целочисленными вершинами, которая содержит s.
LaTeX
$$$\exists B \in \mathrm{Box}(ι), \ operatorname{hasIntegralVertices}(B) \land s \subseteq B$$$
Lean4
/-- Any bounded set is contained in a `BoxIntegral.Box` with integral vertices. -/
theorem le_hasIntegralVertices_of_isBounded [Finite ι] {s : Set (ι → ℝ)} (h : IsBounded s) :
∃ B : BoxIntegral.Box ι, hasIntegralVertices B ∧ s ≤ B :=
by
have := Fintype.ofFinite ι
obtain ⟨R, hR₁, hR₂⟩ := IsBounded.subset_ball_lt h 0 0
let C : ℕ := ⌈R⌉₊
have hC := Nat.ceil_pos.mpr hR₁
let I : Box ι := Box.mk (fun _ ↦ -C) (fun _ ↦ C) (fun _ ↦ by simp [C, neg_lt_self_iff, Nat.cast_pos, hC])
refine ⟨I, ⟨fun _ ↦ -C, fun _ ↦ C, fun i ↦ (Int.cast_neg_natCast C).symm, fun _ ↦ rfl⟩, le_trans hR₂ ?_⟩
suffices Metric.ball (0 : ι → ℝ) C ≤ I from le_trans (Metric.ball_subset_ball (Nat.le_ceil R)) this
intro x hx
simp_rw [C, mem_ball_zero_iff, pi_norm_lt_iff (Nat.cast_pos.mpr hC), Real.norm_eq_abs, abs_lt] at hx
exact fun i ↦ ⟨(hx i).1, le_of_lt (hx i).2⟩
