@[reducible, inline]

abbrev zeroOneBox (n : ℕ) : Set (EuclideanSpace ℝ (Fin n))

Definition 1.3.1: the textbook box B_n = [0,1]^n in ℝⁿ.

@[simp]

theorem mem_zeroOneBox_iff {n : ℕ} {x : EuclideanSpace ℝ (Fin n)} : x ∈ zeroOneBox n ↔ ∀ (i : Fin n), x.ofLp i ∈ Set.Icc 0 1

Membership in zeroOneBox n is exactly the coordinatewise interval condition.

theorem zeroOneBox_zero_mem (n : ℕ) : 0 ∈ zeroOneBox n

The origin belongs to the textbook box B_n = [0,1]^n.