OAI/Analysis/SymmetricDomains/FiberCardAmbientSheets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.continuousOn_padded line 16
  2. theorem OAI.Release061.proper_eventually_fiber_values_close line 37
  3. theorem OAI.Release061.extended_fiber_coefficients line 56
  4. theorem OAI.Release061.monic_eval_as_fin line 112
  5. theorem OAI.Release061.coalescing_coeff_identity line 120
  6. theorem OAI.Release061.finite_fiber_root_identity_extend line 129
  7. theorem OAI.Release061.analytic_coefficient_difference_bound_center line 164
  8. theorem OAI.Release061.coalescing_root_bound_center line 179
  9. theorem OAI.Release061.equicontinuousAt_of_local_coalescing_polynomials line 204
  10. theorem OAI.Release061.fiber_card_of_ambient_sheets line 230