leanprover-community/mathlib4

Prove that inversion is discontinuous at the center

オープン

#5,939 opened on 2023/07/16

GitHub で見るコントリビューターガイド
 (4 件のコメント) (0 件のリアクション) (0 人の担当者)Lean (1,592 件のフォーク)github user discovery
good first issuet-analysist-euclidean-geometryt-topology

Repository metrics

Stars
 (3,869 個のスター)
PR merge metrics
 (30d に merged PR はありません)

説明

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

コントリビューターガイド

調査方針
mathlib4の反転と反射の既存の定義を調べてください。PR #5937のx ≠ cの場合を確認してください。最初のポイントを証明するために、反転がcoboundedに近づくことを示してください。その後、不連続性を導き出し、Fréchet導関数を計算してください。
技術スタック
なし
領域
backend
Issue 種別
調査
難度新しい貢献者にとっての実装難度です。1 は非常に小さな変更、5 は専門的な作業です。
3
推定時間経験ある貢献者が調査、実装、テスト、pull request 準備にかけるおおよその時間範囲です。
1-2日
活動状況Issue が今どれだけ取り組みやすいかを示します。新しい、活発、古い、ブロック中、またはメンテナー入力待ちなどです。
アクティブ
明確さ期待される変更、受け入れ条件、次の手順がどれだけ明確かを示します。
明確
前提条件
GitLean basics
初心者向け度初回貢献者にどれだけ取り組みやすいかを 1-100 で推定したスコアです。
35