leanprover-community/mathlib4

Prove that inversion is discontinuous at the center

Offen

#5.939 geöffnet am 16.07.2023

Auf GitHub ansehenContributor Guide
 (4 Kommentare) (0 Reaktionen) (0 zugewiesene Personen)Lean (1.592 Forks)github user discovery
good first issuet-analysist-euclidean-geometryt-topology

Repository-Metriken

Stars
 (3.869 Sterne)
PR-Merge-Metriken
 (Keine gemergten PRs in 30 T)

Beschreibung

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

Contributor Guide

Research-Richtung
Studiere die vorhandenen Definitionen von Inversion und Reflexion in mathlib4. Untersuche PR #5937 für den Fall x ≠ c. Beweise den ersten Punkt, indem du zeigst, dass die Inversion gegen cobounded tendiert. Leite dann die Diskontinuität ab und berechne die Fréchet Ableitung.
Tech Stack
Keine
Domain
backend
Issue Type
Recherche
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
3
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
1-2 Tage
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Aktiv
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
GitLean basics
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
35