OAI/GroupTheory/PolycyclicRecognition/Analysis/PositiveProjectionCell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_compact_positive_projection_cell line 18

   Source documentation

   A continuous projection admits a compact cell of positive finite mass whose entire projection stays in a prescribed ball.

   theorem exists_compact_positive_projection_cell
       {X Y : Type*} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space X]
       [MeasurableSpace X] [BorelSpace X] [PseudoMetricSpace Y]
       (μ : Measure X) [IsOpenPosMeasure μ] [IsFiniteMeasureOnCompacts μ]
       (q : X → Y) (hq : Continuous q) (x₀ : X) {ρ : ℝ} (hρ : 0 < ρ) :
       ∃ U : Set X, IsCompact U ∧ MeasurableSet U ∧ 0 < μ U ∧ μ U < ⊤ ∧
         ∀ x ∈ U, dist (q x₀) (q x) < ρ := by
   …