OAI/Analysis/DirectCrouzeix/ExtremalEmbedding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectCrouzeix.Conformal.exists_injective_not_dense_image_deriv_ne_zero line 45
2. lemma OAI.DirectCrouzeix.Conformal.exists_mapsTo_unitBall_injOn_deriv_ne_zero line 97
3. structure OAI.DirectCrouzeix.Conformal.NormalizedEmbedding line 123
4. theorem OAI.DirectCrouzeix.Conformal.exists_normalizedEmbedding line 130
5. theorem OAI.DirectCrouzeix.Conformal.extend_restrict_eventuallyEq line 158
6. theorem OAI.DirectCrouzeix.Conformal.exists_extremalEmbedding line 164