Fonctions partielles
Comment spécifier qu'une fonction complexe n'est définie que sur un ouvert ? J'ai une idée pour l'instant : définir un type dépendant :
Definition partiel (U V : C -> Prop) := {x : C | U x} -> {y : C | V y}.
Un objet de type partiel U V
sera une fonction qui prend en argument un complexe, et une preuve que ce complexe est dans U, pour renvoyer un autre complexe, et une preuve de son appartenance à V.
Il faut voir si ça fonctionne bien. Je ne comprend pas exactement comment adapter ton code, donc je pense qu'il vaut mieux que tu essayes de voir. Le problème, c'est que ça nécessite de redéfinir aussi tout ce qu'on a déjà fait (continuité, dérivabilité, etc...)