Revision #1460 → #2112 · back to history
modifiedDomain of definition / natural domainfd1dbaccfc21
| Field | From #1460 | To #2112 |
|---|
| note | `PFun.Dom f` is defined as the set `{a | (f a).Dom}`, the set of inputs on which `f` is defined. | `PFun.Dom f` is the set `{a | (f a).Dom}` of inputs on which `f` is defined. |
modifiedTotal function68271ac06626
| Field | From #1460 | To #2112 |
|---|
| note | Total functions are the ordinary `α → β`; `PFun.lift` coerces them into partial functions with `PFun.dom_coe` showing the domain is `Set.univ`, but no separate `Total` predicate is defined. | Total functions are the ordinary `α → β`; `PFun.lift` coerces them to `PFun` and `PFun.dom_coe` shows the domain is `Set.univ`, but no standalone `Total` predicate is defined on `PFun`. |
modifiedPartial function as univalent relationbd10b97bf4d7
| Field | From #1460 | To #2112 |
|---|
| note | `PFun.graph'` turns a partial function into a `SetRel`, but the converse characterization (univalent relations correspond to partial functions) is not formalized as such. | `PFun.graph'` turns a partial function into a `Set`-valued relation, but the equivalence with univalent relations is not packaged as a theorem. |
modifiedGeneral recursive function74bf54122daa
| Field | From #1460 | To #2112 |
|---|
| note | `Nat.Partrec` is defined as the inductive predicate on `ℕ →. ℕ` capturing partial recursive functions. | `Nat.Partrec` is the inductive predicate on `ℕ →. ℕ` capturing partial recursive functions. |
modifiedSquare root restricted to integers4f25debd0141
| Field | From #1460 | To #2112 |
|---|
| note | No explicit partial function for integer square root restricted to perfect squares is present; `Nat.sqrt` is total. | No explicit partial function for integer square root restricted to perfect squares appears; `Nat.sqrt` is total. |
modifiedSquare root as partial function on reals6fc611f94528
| Field | From #1460 | To #2112 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Pow.Real | Mathlib.Analysis.Real.Sqrt |
| note | `Real.sqrt` is total in Mathlib (returns 0 on negatives) rather than encoded as a partial function on ℝ. | `Real.sqrt` is total in Mathlib (returns 0 on negatives) rather than encoded as a `PFun` on ℝ. |
modifiedDomain of definition (subset S)589f57fe1ce3
| Field | From #1460 | To #2112 |
|---|
| note | Same as the `PFun.Dom` declaration above, a `Set α` subset on which `f` is defined. | Same `PFun.Dom` declaration: a `Set α` consisting of the inputs on which `f` is defined. |
modifiedTotal partial function02b5021ea31f
| Field | From #1460 | To #2112 |
|---|
| note | `PFun.dom_coe` shows lifted (total) functions have `Dom = Set.univ`, but there is no standalone `PFun.Total` predicate. | `PFun.dom_coe` shows lifted total functions have `Dom = Set.univ`, but no standalone `PFun.Total` predicate is defined. |
modifiedInjective/surjective/bijective partial function0b018bdca7bc
| Field | From #1460 | To #2112 |
|---|
| note | No `PFun.Injective`/`PFun.Surjective`/`PFun.Bijective` predicate exists; `PFun.asSubtype` lets one state these via `Function.Injective` etc., but the named predicates are absent. | No `PFun.Injective`/`PFun.Surjective`/`PFun.Bijective` predicate exists; one can express these via `PFun.asSubtype` and `Function.Injective`, but the named predicates are absent. |
modifiedInversion of injective partial functions67f30b65f18a
| Field | From #1460 | To #2112 |
|---|
| note | `PEquiv.symm` inverts a partial bijection to another partial bijection, but no general inversion theorem for injective `PFun`s is stated. | `PEquiv.symm` inverts a partial bijection to another partial bijection, but no general inversion theorem for an injective `PFun` is stated. |
addedInjection invertible to bijective partial functiond5b61797901a
modifiedPartial transformationeacf64da45f2
| Field | From #1460 | To #2112 |
|---|
| note | A partial transformation `α →. α` is a special case of `PFun α α`, but there is no dedicated `PartialTransformation` name. | A partial transformation `α →. α` is a special case of `PFun α α`, but no dedicated `PartialTransformation` name exists. |
modifiedCardinality of partial function set0e027bef483e
| Field | From #1460 | To #2112 |
|---|
| note | No cardinality formula `|Y∪{∗}|^|X|` for `PFun X Y` is stated in Mathlib. | No cardinality formula `(|Y|+1)^|X|` for `PFun X Y` in the finite case is stated in Mathlib. |
modifiedNatural logarithmd7bf496e5ef3
| Field | From #1460 | To #2112 |
|---|
| note | `Real.log` is defined as a total function (zero on non-positives) rather than a `PFun`. | `Real.log` is defined as a total function (zero on non-positives) rather than as a `PFun`. |
modifiedSubtraction of natural numbersd7299690a7e5
| Field | From #1460 | To #2112 |
|---|
| note | `Nat.sub` is a total truncated subtraction in Mathlib/core, not modeled as a `PFun`. | `Nat.sub` is a total truncated subtraction in core/Mathlib, not modeled as a `PFun`. |
modifiedBottom element semantics79c0299cfbcd
| Field | From #1460 | To #2112 |
|---|
| note | `Part.none` plays the role of the bottom/undefined value for `Part`-valued partial functions, but no explicit denotational `⊥` semantics is developed. | `Part.none` plays the role of the bottom/undefined value for `Part`-valued partial functions, but no explicit denotational ⊥-semantics framework is developed. |
modifiedEquivalence with pointed sets966293386136
| Field | From #1460 | To #2112 |
|---|
| note | `partialFunEquivPointed : PartialFun ≌ Pointed` gives the (noncomputable, classical) equivalence between the categories. | `partialFunEquivPointed : PartialFun ≌ Pointed` gives the categorical equivalence between sets-with-partial-functions and pointed sets. |
modifiedSelf-duality of partial bijections categorye2bcb29d02dc
| Field | From #1460 | To #2112 |
|---|
| note | No category of sets-with-partial-bijections nor its self-duality is formalized. | Neither the category of sets-with-partial-bijections nor its self-duality is formalized. |
modifiedCharts in atlases as partial functionsa1111b20c7af
| Field | From #1460 | To #2112 |
|---|
| note | `ChartedSpace H M` has an atlas of `OpenPartialHomeomorph`s (partial homeomorphisms with open source/target), which embodies the chart-as-partial-function idea but uses `PartialHomeomorph`/`PartialEquiv` rather than `PFun`. | `ChartedSpace H M` has an atlas of `OpenPartialHomeomorph`s, embodying charts-as-partial-functions but via partial homeomorphisms rather than via `PFun`. |
addedTransition map3b0454e34f0a