Closed cubes in ℝ^d are closed

Proved

DbarRegularity.isClosed_closedCube

by Mazecto · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

euclidean-spaceharmonic-analysistopology

For every $a\in\mathbb{R}^d$ and $s\in\mathbb{R}$ , the closed cube

Q(a,s)=\{x\in\mathbb{R}^d:\ a_i\le x_i\le a_i+s\ \text{for all } i\}

is a closed subset of $\mathbb{R}^d$ .

Formalization Note. closedCube a s comes from Definitions.Def_DbarRegularity_Setting; $\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) with its Euclidean topology.

Preamble

import Definitions.Def_DbarRegularity_Setting

Formal statement

namespace DbarRegularity

/-- The closed cube `∏ᵢ [aᵢ, aᵢ + s]` is a closed subset of `ℝ^d`. -/
theorem isClosed_closedCube {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (s : ℝ) :
    IsClosed (closedCube a s) := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapter I, § 3.2, p. 16

View graph