OAI/Analysis/DirectCrouzeix/NormalFamilies.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.Conformal.zero_or_nonvanishing_limit line 27
  2. theorem OAI.DirectCrouzeix.Conformal.constant_or_injective_limit line 86
  3. def OAI.DirectCrouzeix.Conformal.extend line 120
  4. theorem OAI.DirectCrouzeix.Conformal.extend_coe line 124
  5. theorem OAI.DirectCrouzeix.Conformal.continuousMap_limit line 127
  6. theorem OAI.DirectCrouzeix.Conformal.bounded_holomorphic_equicontinuous line 135
  7. theorem OAI.DirectCrouzeix.Conformal.bounded_holomorphic_compact line 179
  8. theorem OAI.DirectCrouzeix.Conformal.bounded_holomorphic_closure line 203
  9. theorem OAI.DirectCrouzeix.Conformal.derivative_continuousOn line 217
  10. theorem OAI.DirectCrouzeix.Conformal.strict_bound_of_normalized line 230