OAI/Analysis/SymmetricDomains/ProperEventuallyFiberSubset.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.fiber_card_of_sheets line 15
  2. theorem OAI.Release061.coeff_X_sub_C_mul_all line 32
  3. theorem OAI.Release061.analyticAt_coeff_prod_X_sub_C line 38
  4. theorem OAI.Release061.norm_coeff_prod_X_sub_C_le line 56
  5. theorem OAI.Release061.monic_natDegree_prod_X_sub_C line 77
  6. theorem OAI.Release061.exists_vector_prod_X_sub_C line 84
  7. theorem OAI.Release061.continuous_coeff_prod_fin line 95
  8. theorem OAI.Release061.tendsto_coeff_prod_of_values_coalesce line 104
  9. def OAI.Release061.ScalarAnalyticAt line 131
  10. theorem OAI.Release061.ScalarAnalyticAt.continuousAt line 135
  11. theorem OAI.Release061.ScalarAnalyticAt.congr line 140
  12. theorem OAI.Release061.scalarAnalyticAt_const line 146
  13. theorem OAI.Release061.ScalarAnalyticAt.comp line 150
  14. theorem OAI.Release061.scalarAnalyticAt_padded line 161
  15. theorem OAI.Release061.fiberPolynomial_coeff_analyticAt_of_sheets line 177
  16. theorem OAI.Release061.proper_eventually_fiber_subset line 225