Theorems · Theorem · measure theory

MeasureTheory.hausdorffMeasure_orthogonalProjectionOnto_le

∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (K : Submodule 𝕜 E) [inst_5 : K.HasOrthogonalProjection] (d : ℝ)
  (s : Set E),
  0 ≤ d →
    (MeasureTheory.Measure.hausdorffMeasure d) (⇑K.orthogonalProjectionOnto '' s) ≤
      (MeasureTheory.Measure.hausdorffMeasure d) s

Let s be a subset of 𝕜-inner product space, and K a subspace. Then the d-dimensional Hausdorff measure of the orthogonal projection of s onto K is less than or equal to the d-dimensional Hausdorff measure of s.

Defined in

Mathlib.MeasureTheory.Measure.Hausdorff

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceSubmodule.HasOrthogonalProjection