OAI/Analysis/RieszRectifiability/Nets/LatticeDescendantGeometry.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.RieszRectifiability.SupportCellDescendantline 13 - def
OAI.RieszRectifiability.SupportCellDescendant.radiusline 23 - def
OAI.RieszRectifiability.SupportCellDescendant.binaryLevelline 25 - def
OAI.RieszRectifiability.SupportCellDescendant.cellline 27 - theorem
OAI.RieszRectifiability.SupportCellDescendant.radius_posline 30 - theorem
OAI.RieszRectifiability.SupportCellDescendant.center_mem_supportline 33 - theorem
OAI.RieszRectifiability.SupportCellDescendant.center_dist_topline 36 - theorem
OAI.RieszRectifiability.SupportCellDescendant.binary_radiusline 43 - theorem
OAI.RieszRectifiability.SupportCellDescendant.scale_eqline 52 - theorem
OAI.RieszRectifiability.SupportCellDescendant.separatedline 58 - theorem
OAI.RieszRectifiability.SupportCellDescendant.core_admissibleline 78 - theorem
OAI.RieszRectifiability.SupportCellDescendant.cell_subset_topline 87