OAI/MeasureTheory/Falconer/Geometry/BoundedChartFineGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Extend the checked regular gain to the full bounded point chart by a second fixed contraction, preserving the original finite union.

  1. theorem OAI.Falconer.bounded_chart_regular_fine_gain line 10