OAI/Analysis/RieszRectifiability/Foundations/IndexedSeedChainCounting.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Counting indexed captured seed chains

Injective levels reduce a finite indexed family to a chain of natural-number levels. Bounded seed offsets and the marked gaps then control the size of the original family.

  1. theorem OAI.RieszRectifiability.indexed_captured_seed_chain_count line 15