OAI/Analysis/RieszRectifiability/Foundations/SupportDescendantCountable.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Countability of support-cell descendants

Every descendant is determined by its depth and its center in the corresponding support lattice net. Encoding these data in a countable dependent sum proves countability of the full descendant family, not only of each generation.

  1. theorem OAI.RieszRectifiability.supportCellDescendant_countable line 20