OAI/Geometry/IsometricImmersion/Estimates/HighFactorOrders.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.HighEquation.ordered_partSize_sum line 11
  2. theorem OAI.SmoothLocal.HighEquation.ordered_two_partSizes_le line 16
  3. theorem OAI.SmoothLocal.HighEquation.high_factor_spends line 24
  4. theorem OAI.SmoothLocal.HighEquation.ordered_high_factor_unique line 28
  5. theorem OAI.SmoothLocal.HighEquation.ordered_high_factor_card_le_one line 40
  6. theorem OAI.SmoothLocal.HighEquation.ordered_other_factor_order_le line 49
  7. theorem OAI.SmoothLocal.HighEquation.remaining_factor_order_le line 58
  8. theorem OAI.SmoothLocal.HighEquation.ordered_top_factor_classes line 62
  9. theorem OAI.SmoothLocal.HighEquation.ordered_penultimate_other_singleton line 70
  10. theorem OAI.SmoothLocal.HighEquation.ordered_remainder_factor_orders line 78
  11. theorem OAI.SmoothLocal.HighEquation.ordered_extracted_factor_orders line 86