OAI/Geometry/IsometricImmersion/Calculus/QuotientLowBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.LowQuotient.bound0 line 13
  2. def OAI.SmoothLocal.Geometry.LowQuotient.bound1 line 14
  3. def OAI.SmoothLocal.Geometry.LowQuotient.bound2 line 15
  4. def OAI.SmoothLocal.Geometry.LowQuotient.bound3 line 16
  5. def OAI.SmoothLocal.Geometry.LowQuotient.boundThroughThree line 18
  6. theorem OAI.SmoothLocal.Geometry.LowQuotient.bounds_nonneg line 20
  7. theorem OAI.SmoothLocal.Geometry.LowQuotient.abs_add_bound line 24
  8. theorem OAI.SmoothLocal.Geometry.LowQuotient.abs_mul_bound line 27
  9. theorem OAI.SmoothLocal.Geometry.LowQuotient.abs_sub_bound line 32
  10. theorem OAI.SmoothLocal.Geometry.LowQuotient.abs_div_bound line 35
  11. theorem OAI.SmoothLocal.Geometry.LowQuotient.denominator_ne_zero line 42
  12. theorem OAI.SmoothLocal.Geometry.LowQuotient.quotient_bound_zero line 49
  13. theorem OAI.SmoothLocal.Geometry.LowQuotient.quotient_bound_one line 62
  14. theorem OAI.SmoothLocal.Geometry.LowQuotient.quotient_bound_two line 70
  15. theorem OAI.SmoothLocal.Geometry.LowQuotient.quotient_bound_three line 91
  16. theorem OAI.SmoothLocal.Geometry.LowQuotient.quotient_bound_through_three line 125