OAI/Geometry/ProjectionBody/NullHyperplane.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.volume_linear_level_eq_zero line 11

   Source documentation

   Every level set of a nonzero real linear functional has zero ambient volume.

   theorem volume_linear_level_eq_zero
       {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
       [FiniteDimensional ℝ V] [MeasureSpace V] [BorelSpace V]
       [Measure.IsAddHaarMeasure (volume : Measure V)]
       (f : V →ₗ[ℝ] ℝ) (hf : f ≠ 0) (c : ℝ) :
       volume {x : V | f x = c} = 0 := by
   …