Revision #1242 → #2075 · back to history
modifiedGraph of a function152466608f49
| Field | From #1242 | To #2075 |
|---|
| note | `Function.graph f = {(a, b) | f a = b}` matches the graph definition, and `graph_injective` shows the representation is unique. | `Function.graph f = {(a, b) | f a = b}` matches the graph definition. |
modifiedImage of a function (range)dcfac4e461b5
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Data.Set.Image | Mathlib.Data.Set.Operations |
addedSquare functione7da9953bdfd
addedCartesian product of two sets552171791a76
addedRiemann zeta function and Riemann hypothesis9ebba17313e9
modifiedUndecidability of recursive-function membership (Halting problem)21d5cc3509bd
| Field | From #1242 | To #2075 |
|---|
| mathlib.decl | Computability.halting_problem | ComputablePred.halting_problem |
| note | `halting_problem` proves `¬ComputablePred fun c => (eval c n).Dom`, the undecidability of the halting predicate. | `ComputablePred.halting_problem` proves `¬ComputablePred fun c => (c.eval n).Dom`, the undecidability of the halting predicate. |
modifiedMultiplication of integers as bivariate function98914ee1e68a
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Data.Int.Defs | Init.Data.Int.Basic |
| note | Integer multiplication is realized as a binary function via the `Mul ℤ` instance. | Integer multiplication is realized as a binary function via `Int.mul` (and the `Mul ℤ` instance). |
modifiedCartesian product of n setsbfd8c5ca88c1
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Data.Set.Prod | Mathlib.Data.Set.Operations |
addedNatural logarithm as bijection; exponential as inversef1951ab5895f
addedArccosine as inverse of restricted cosinec07edf68b16a
modifiedImplicit function theoremc725fd684d05
| Field | From #1242 | To #2075 |
|---|
| note | `HasStrictFDerivAt.implicitFunction` and its `prodFun_implicitFunction` equation provide the implicit function theorem in Banach spaces. | `HasStrictFDerivAt.implicitFunction` provides the implicit function theorem in Banach spaces. |
modifiedFunction defined as an antiderivative38fde9aadf2e
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Integral.IntervalIntegral | Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic |
modifiedExponential function as solution of a differential equation1ff8034f78de
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Exp | Mathlib.Analysis.Complex.Exponential |
modifiedEmpty functiona33480fa3b47
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Logic.IsEmpty.Basic | Mathlib.Logic.IsEmpty.Defs |
modifiedCanonical surjection onto imagefb347c417b2a
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Data.Set.Image | Mathlib.Data.Set.Operations |
modifiedIdentity functions are left/right identities7f525dcf955d
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Logic.Function.Defs | Init.Core |
modifiedFiber of a point46e51dd712df
| Field | From #1242 | To #2075 |
|---|
| note | The fiber of `y` under `f` is `f ⁻¹' {y}`; `Function.fiber` in Mathlib.Logic.Function.FiberPartition packages this for partitioning. | The fiber of `y` under `f` is `f ⁻¹' {y}`, a special case of `Set.preimage`. |
modifiedBijective iff admits an inverse function44255e872fc5
| Field | From #1242 | To #2075 |
|---|
| note | Mathlib proves bijective is equivalent to having a two-sided inverse (`leftInverse_surjInv`/`rightInverse_surjInv`), and `Equiv.ofBijective` packages the inverse. | `Function.bijective_iff_has_inverse` proves that bijective is equivalent to having a two-sided inverse. |
modifiedCanonical factorization of a function930ea2a5483c
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Data.Set.Image | Mathlib.Data.Set.Operations |
addedAnalytic continuationcf729b77b16c
modifiedPointwise operations on real functions1be3a1c2437f
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Pi.Basic | Mathlib.Algebra.Notation.Pi.Defs |
modifiedMonotonic real function485a3bd097e9
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Order.Defs | Mathlib.Order.Monotone.Defs |
addedSine and cosine as solutions of the linear ODE y'' = -y0cdd7397af3d
modifiedFunction spaceb5e4b569b431
| Field | From #1242 | To #2075 |
|---|
| mathlib.module | Mathlib.Topology.ContinuousMap.Basic | Mathlib.Topology.ContinuousMap.Defs |
modifiedEquivalence of models of computation; Church–Turing thesis1a6110c6ac64
| Field | From #1242 | To #2075 |
|---|
| mathlib.decl | Turing.Partrec.to_TM2 | Turing.PartrecToTM2.tr_eval |
| note | Mathlib formalizes equivalences between partial-recursive functions and Turing machine models in `Computability/TuringMachine/ToPartrec`, but a comprehensive Church-Turing equivalence covering all standard models is not packaged. | `Turing.PartrecToTM2.tr_eval` formalizes that a TM2 machine simulates partial-recursive evaluation, but a comprehensive Church-Turing equivalence covering all standard models is not packaged. |