OAI/MeasureTheory/Falconer/Incidence/LocalPencilPacketGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Assemble the separately selected original cell pencils into one packet. The pointwise choice preserves the common original tube cover.

  1. theorem OAI.Falconer.centered_packet_gain_from_local_pencils line 10