Port to MathComp 2 #951
Merged
Port to MathComp 2 #951
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Co-authored-by: Cyril Cohen <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
* quotient topology * docs * trying to fix build * cleaning up proof * more general quotients * docs * trying to fix build * nitpicks * quotType alias * fix changelog * fixing changelog again --------- Co-authored-by: Reynald Affeldt <[email protected]>
* swapping machines * proof of open map * hausdorff accessible * weak products equivalent * changelog * strengthen join_product_weak * cleaning up proofs * typos * adding local notations for proof legibility * merging product stuff * fixing changelog * specialized conjunctions to use less brackets and splits * fixing grammar * fix changelog * fixing build * more build fixes --------- Co-authored-by: Reynald Affeldt <[email protected]>
- use cover in finSubCover - use [set: ] instead of @Sett - use shortcut notation for set comprehension
* proving sups preserve countable ent * proof going through * unused proofs * linting * metric implies countable uniformity * fixing changelog * linting * metric for products * linting * fixing docs * use %:pos * fixing changelog * fix changelog * nitpicking --------- Co-authored-by: Reynald Affeldt <[email protected]>
* simplifying clopen proofs * clopen separations * adding docs * linting. * nitpicks, trailing spaces, lint --------- Co-authored-by: Reynald Affeldt <[email protected]>
* cluster1 proof * updating changelog * Update theories/topology.v Co-authored-by: affeldt-aist <[email protected]> * Update theories/topology.v Co-authored-by: affeldt-aist <[email protected]> * change to signature of compact_near_coveringP * no need to name intermediate hypo --------- Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
* add a type for finite measures - s-finite measures from branch kernels - add subprobabilities - dirac instance of probability - rm finite_measure - renaming - minor fix
Co-authored-by: Quentin Vermande <[email protected]>
- a few pinfty/ninfty -> y/Ny renamings
* Add itv.v Taking inspiration on signed.v, replacing sign by intervals. * Add interval multiplication * Add hints to automatically solve _ <= 1 goals * Test to see if usable as a replacement for prob * use notation from mathcomp_extra.v * changelog and rm redundant code * prefix duplicated identifiers --------- Co-authored-by: Reynald Affeldt <[email protected]>
* more opam keywords (MCA-dev meeting of 2023-12-21)
* fixes #1123 Co-authored-by: Takafumi Saikawa <[email protected]> Co-authored-by: Zachary Stone <[email protected]>
* Radon_Nikodym chain rule --------- Co-authored-by: IshiguroYoshihiro <[email protected]> Co-authored-by: IshiguroYoshihiro <[email protected]> Co-authored-by: Tragicus <[email protected]>
* format doc --------- Co-authored-by: Pierre Roux <[email protected]>
Co-authored-by: Kazuhiko Sakaguchi <[email protected]>
* isolate the theory of lime_sup - generic def of limsup --------- Co-authored-by: Zachary Stone <[email protected]>
* helper lemmas for contra (PR #1119) * rm pdegen, use more PropB --------- Co-authored-by: Reynald Affeldt <[email protected]>
* test a few files
* generalizations
* curry/uncurry of continuous functions * compact-open topology working * removing regular in favor of regular_space --------- Co-authored-by: Reynald Affeldt <[email protected]>
Co-authored-by: Georges Gonthier <[email protected]>
* total variation proofs - increasing implies BV - splitting partitions - right/left continuity of TV - define variation with path - adding monotone variation - variation using prev and next --------- Co-authored-by: Reynald Affeldt <[email protected]>
* changelog for version 0.7.0
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I realize we have the branch but not the PR, so here it is just to keep track of it.
Things done/to do
CHANGELOG_UNRELEASED.md