OAI/MeasureTheory/Falconer/Recursion/ScalarTerminalProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A terminal fiber contributes its full cardinality to every sum projection. This is the base case for keeping whole terminal clusters.

  1. theorem OAI.Falconer.scalar_sum_cells_card_left line 10