leanprover-community/mathlib4

Prove that inversion is discontinuous at the center

Ouverte

#5 939 ouverte le 16 juil. 2023

Voir sur GitHubGuide contributeur
 (4 commentaires) (0 réaction) (0 personne assignée)Lean (1 592 forks)github user discovery
good first issuet-analysist-euclidean-geometryt-topology

Métriques du dépôt

Stars
 (3 869 étoiles)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

Description

  • Prove Tendsto (inversion c R) (𝓝[≠] c) cobounded if R ≠ 0.
  • Deduce that inversion c R is discontinuous at c if R ≠ 0 and the vector space is nontrivial.
  • Deduce that fderiv (inversion c R) c is zero, thus fderiv (inversion c R) x = ((R / dist x c) ^ 2 • (reflection (ℝ ∙ (x - c))ᗮ : F →L[ℝ] F)) x for all x (see #5937 for the case x ≠ c).

Guide contributeur

Direction de recherche
Étudiez les définitions existantes de l'inversion et de la réflexion dans mathlib4. Examinez la PR #5937 pour le cas x ≠ c. Démontrez le premier point en montrant que l'inversion tend vers cobounded. Déduisez ensuite la discontinuité et calculez la dérivée de Fréchet.
Stack technique
Aucun
Domaine
backend
Type d'issue
Recherche
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-2 jours
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
GitLean basics
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
35