Theorems · Theorem · measure theory

MeasureTheory.measure_le_eq_lt

∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [FiniteDimensional ℝ E] [mE : MeasurableSpace E]
  [tE : TopologicalSpace E] [IsTopologicalAddGroup E] [BorelSpace E] [T2Space E] [ContinuousSMul ℝ E]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {g : E → ℝ},
  g 0 = 0 →
    (∀ (x : E), g (-x) = g x) →
      (∀ (x y : E), g (x + y) ≤ g x + g y) →
        (∀ {x : E}, g x = 0 → x = 0) →
          (∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x) → ∀ [Nontrivial E] (r : ℝ), μ {x | g x ≤ r} = μ {x | g x < r}

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Cited by

3 results in Mathlib

Foundations

Depth 263 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModuleFiniteDimensionalMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpaceT2SpaceContinuousSMulMeasureTheory.Measure.IsAddHaarMeasureNontrivial