|
93 | 93 | + lemma `is_diff_mx` |
94 | 94 | + instance `is_diff_mx` |
95 | 95 |
|
96 | | -- in `mathcomp_extra.v`: |
97 | | - + lemmas `divDl_ge0`, `divDl_le1` |
98 | | - + mixin `Zmodule_isSubNormed` |
99 | | - + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) |
100 | | - |
101 | | -- in `unstable.v`: |
102 | | - + lemmas `divD_onem` |
103 | | - |
104 | | -### Changed |
105 | | - |
106 | | -- moved from `measurable_structure.v` to `classical_sets.v`: |
107 | | - + definition `preimage_set_system` |
108 | | - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, |
109 | | - `preimage_set_system_id` |
110 | 96 | - in `functions.v`: |
111 | 97 | + lemmas `linfunP`, `linfun_eqP` |
112 | 98 | + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }` |
|
131 | 117 |
|
132 | 118 | - new files `signed_measure.v` and `radon_nikodym.v` |
133 | 119 | + with the contents of `charge.v` (deprecated) |
134 | | - |
| 120 | + |
| 121 | +- in `mathcomp_extra.v`: |
| 122 | + + lemmas `divDl_ge0`, `divDl_le1` |
| 123 | + + mixin `Zmodule_isSubNormed` |
| 124 | + + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) |
| 125 | + |
| 126 | +- in `unstable.v`: |
| 127 | + + lemmas `divD_onem` |
| 128 | + |
135 | 129 | ### Changed |
136 | 130 |
|
| 131 | +- moved from `measurable_structure.v` to `classical_sets.v`: |
| 132 | + + definition `preimage_set_system` |
| 133 | + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, |
| 134 | + `preimage_set_system_id` |
| 135 | + |
137 | 136 | - moved from `measurable_structure.v` to `classical_sets.v`: |
138 | 137 | + definition `preimage_set_system` |
139 | 138 | + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, |
|
0 commit comments