leanprover-community/mathlib4

Prove that inversion is discontinuous at the center

Aperta

#5939 aperta il 16 lug 2023

Vedi su GitHubGuida contributor
 (4 commenti) (0 reazioni) (0 assegnatari)Lean (1592 fork)github user discovery
good first issuet-analysist-euclidean-geometryt-topology

Metriche repository

Star
 (3869 stelle)
Metriche merge PR
 (Nessuna PR mergiata in 30 g)

Descrizione

  • 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).

Guida contributor

Direzione di ricerca
Studia le definizioni esistenti di inversione e riflessione in mathlib4. Esamina la PR #5937 per il caso x ≠ c. Dimostra il primo punto mostrando che l'inversione tende a cobounded. Quindi deduci la discontinuità e calcola la derivata di Fréchet.
Tech stack
Nessuno
Dominio
backend
Tipo issue
Ricerca
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
GitLean basics
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
35