OAI/Analysis/RieszRectifiability/Nets/CellChainComposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RieszRectifiability.SupportCellDescendant.eq_of_common_point_same_depth line 12
  2. theorem OAI.RieszRectifiability.SupportCellDescendant.cell_nested_of_common_point line 27
  3. theorem OAI.RieszRectifiability.supportLatticeAncestor_eq_of_center_mem line 35
  4. def OAI.RieszRectifiability.SupportCellDescendant.compose line 45
  5. theorem OAI.RieszRectifiability.SupportCellDescendant.compose_depth line 57
  6. theorem OAI.RieszRectifiability.SupportCellDescendant.compose_cell line 63
  7. theorem OAI.RieszRectifiability.SupportCellDescendant.compose_radius line 71
  8. theorem OAI.RieszRectifiability.SupportCellDescendant.exists_relative_descendant line 78