Ball Topology

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.isOpen_euclideanBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : IsOpen (euclideanBall x₀ R)

The open Euclidean ball is open in the product topology.

theorem CKN.measurableSet_euclideanBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : MeasurableSet (euclideanBall x₀ R)

The open Euclidean ball is a measurable set.

theorem CKN.euclideanBall_subset_metricBall {d : ℕ} {x₀ : Vec d} {R : ℝ} (hR : 0 < R) : euclideanBall x₀ R ⊆ Metric.ball x₀ R

The open Euclidean ball is contained in the metric ball with the same radius.

theorem CKN.volume_euclideanBall_lt_top {d : ℕ} (x₀ : Vec d) {R : ℝ} (hR : 0 < R) : MeasureTheory.volume (euclideanBall x₀ R) < ⊤

The volume of the open Euclidean ball is finite.

theorem CKN.volume_euclideanBall_ne_top {d : ℕ} (x₀ : Vec d) {R : ℝ} (hR : 0 < R) : MeasureTheory.volume (euclideanBall x₀ R) ≠ ⊤

The volume of the open Euclidean ball is not infinite.

theorem CKN.volume_euclideanBall_pos {d : ℕ} (x₀ : Vec d) {R : ℝ} (hR : 0 < R) : 0 < MeasureTheory.volume (euclideanBall x₀ R)

The volume of the open Euclidean ball is positive.