Revision #1387 → #1838 · back to history
modifiedMathematical induction3f460946b5d3
| Field | From #1387 | To #1838 |
|---|
| note | The principle of mathematical induction on ℕ is built into Lean as Nat.rec; Mathlib's Nat.le_induction in Mathlib.Data.Nat.Init packages the usual ‘base + step’ form. | The principle of mathematical induction on ℕ is built into Lean as Nat.rec; Mathlib's Nat.le_induction in Mathlib.Data.Nat.Init packages the usual 'base + step' form. |
modifiedStructural induction1ba15c295327
| Field | From #1387 | To #1838 |
|---|
| mathlib.module | Mathlib.Order.WellFounded | Init.WF |
| note | Structural induction is realized via Lean's auto-generated .rec principles and Mathlib's WellFounded.induction (see Mathlib/Order/WellFounded.lean). | Structural induction is realized via Lean's auto-generated .rec principles and WellFounded.induction (Init.WF, re-exported by Mathlib.Order.WellFounded). |
modifiedTrigonometric inequality |sin nx| ≤ n|sin x|49d95e2ea571
| Field | From #1387 | To #1838 |
|---|
| note | Grep for sin patterns in Mathlib/Analysis turned up |sin x| ≤ |x| and Lipschitz bounds but no |sin (n·x)| ≤ n |sin x| statement. | Loogle for the conclusion pattern and grep of Mathlib's trigonometry files turned up |sin x| ≤ |x| (Real.abs_sin_le_abs) and Lipschitz bounds but no |sin (n·x)| ≤ n |sin x| statement. |
modifiedInduction on more than one counteraebdf6f21a51
| Field | From #1387 | To #1838 |
|---|
| mathlib.decl | Prod.lex_wf | Prod.Lex.instIsWellFounded |
| note | Double induction is realized via product/lexicographic well-foundedness; Mathlib/Order/RelClasses.lean shows induction in two variables using WellFoundedLT.induction nested. | Double induction is realized via product/lexicographic well-foundedness; Prod.Lex.instIsWellFounded in Mathlib/Order/RelClasses.lean gives the well-foundedness needed for nested induction on two counters. |
modifiedMethod of infinite descentc16ef9429330
| Field | From #1387 | To #1838 |
|---|
| note | Mathlib has WellFounded.induction_bot / induction_bot' (Mathlib/Order/WellFounded.lean) capturing the descent principle, but no decl named ‘infinite descent’ was found. | Mathlib has WellFounded.induction_bot in Mathlib/Order/WellFounded.lean capturing the descent principle, but no decl named 'infinite descent' was found. |
modifiedFibonacci numbers via complete induction1674dfbe86ba
| Field | From #1387 | To #1838 |
|---|
| note | Mathlib defines Nat.fib by ordinary recursion and proves many lemmas using induction, but there is no headline example labelled ‘Fibonacci via strong induction’. | Mathlib defines Nat.fib by ordinary recursion and proves many lemmas using induction, but there is no headline example labelled 'Fibonacci via strong induction'. |
modifiedPrime factorization via complete induction4a17a7349d76
| Field | From #1387 | To #1838 |
|---|
| mathlib.module | Mathlib.Data.Nat.Prime.Basic | Mathlib.Data.Nat.Prime.Defs |
modifiedForward-backward induction16584bf3d61b
| Field | From #1387 | To #1838 |
|---|
| note | Nat.decreasingInduction in Mathlib/Data/Nat/Init.lean provides downward induction, the ‘backward’ half of Cauchy's forward-backward scheme. | Nat.decreasingInduction in Mathlib/Data/Nat/Init.lean provides downward induction, the 'backward' half of Cauchy's forward-backward scheme. |
modifiedInduction in ZFC set theorye08a0e11af8d
| Field | From #1387 | To #1838 |
|---|
| anchors | [{"section":"Formalization","snippet":"In first-order ZFC set theory , quantification over predicates is not allowed, but one can still express induction by quantification over sets:"},{"type":"math_alttext","value":"{\\displaystyle \\forall A{\\Bigl (}0\\in A\\land \\forall k\\in \\mathbb {N} {\\bigl (}k\\in A\\to (k+1)\\in A{\\bigr )}\\to \\mathbb {N} \\subseteq A{\\Bigr )}}"}] | [{"section":"Formalization","snippet":"In first-order ZFC set theory , quantification over predicates is not allowed, but one can still express induction by quantification over sets:"},{"type":"math_alttext","value":"{\\displaystyle \\forall A{\\Bigl (}0\\in A\\land \\forall k\\in \\mathbb {N} {\\bigl (}k\\in A\\to (k+1)\\in A{\\bigr )}\\to \\mathbb {N} \\subseteq A{\\Bigr )}"}] |
modifiedTransfinite inductione3c9ee03b85c
| Field | From #1387 | To #1838 |
|---|
| mathlib.module | Mathlib.Order.WellFounded | Init.WF |
| note | WellFounded.induction (and Ordinal.induction in Mathlib/SetTheory/Ordinal) provide the transfinite/well-founded induction principle. | WellFounded.induction (Init.WF, re-exported in Mathlib.Order.WellFounded) provides the transfinite/well-founded induction principle. |
modifiedInduction implies well-ordering principle648a29e456eb
| Field | From #1387 | To #1838 |
|---|
| mathlib.decl | wellFounded_iff_has_min | WellFounded.wellFounded_iff_has_min |
| note | Mathlib proves the equivalence well-founded ↔ every nonempty set has a minimum element (wellFounded_iff_has_min), implicitly the natural-number equivalence between induction and well-ordering. | Mathlib proves the equivalence well-founded ↔ every nonempty set has a minimum element (WellFounded.wellFounded_iff_has_min), implicitly the natural-number equivalence between induction and well-ordering. |
addedSum of first n odd integers equals n²de471d07bab7
addedAM-GM inequality (Cauchy's forward-backward proof)dd7de9d787d3