Introduce a notion of inverse_map f g which holds for maps f : X → Y, g : Y → X if they are inverses of eachother.
Redefine invertible, homeomorphism, FiniteT and eq_cardinal in terms of inverse_map. This allows for more better reuse of statements.
Change the def. of topological_property to use homeomorphic instead of homeomorphism. This makes it easier to apply proofs of topological_property. Use Build_topological_property as boilerplate when proving something is a topological_property.
Change the order of imports, so that FiniteTypes includes Cardinals instead of the other way around. This way we can prove general statements about eq_cardinal and le_cardinal and then use them for Finite and FiniteT. Previously the proofs would've been duplicated.
Split the theory of eq_cardinal and le_cardinal into multiple files in the folder Cardinals. They are all exported in the file Cardinals.v
Left to do:
[x] Adapt meta.yml and the README.md to reflect the new structure of the files.
[ ] Can Finite_as_lt_cardinal_ens and injective_finite_inverse_image be proven in a way such that they can be moved to Finite_sets? That is, without using FiniteT or nat_unbounded_impl_countably_infinite.
This big restructuring of the library comes from some Yak shaving.
I wanted to characterize some spaces up to homeomorphism, so I wanted to have appropriate definitions of homeomorphism, homeomorphic and topological_property.
I started by redefining homeomorphisms, noting that a property inverse_map would be useful in proofs about it.
But then it makes sense to redefine invertible in terms of inverse_map, instead of doing its own thing with Inductive.
This leads to many changes in proofs about FiniteT.
By noting that bij_finite uses something like eq_cardinal, by redefining eq_cardinal to use invertible as well, we can extract the lemmas of eq_cardinal _ _ from FiniteTypes and state them separately.
This branch does:
inverse_map f gwhich holds for mapsf : X → Y,g : Y → Xif they are inverses of eachother.invertible,homeomorphism,FiniteTandeq_cardinalin terms ofinverse_map. This allows for more better reuse of statements.topological_propertyto usehomeomorphicinstead ofhomeomorphism. This makes it easier to apply proofs oftopological_property. UseBuild_topological_propertyas boilerplate when proving something is atopological_property.eq_cardinalandle_cardinaland then use them forFiniteandFiniteT. Previously the proofs would've been duplicated.eq_cardinalandle_cardinalinto multiple files in the folderCardinals. They are all exported in the fileCardinals.vLeft to do:
meta.ymland theREADME.mdto reflect the new structure of the files.Finite_as_lt_cardinal_ensandinjective_finite_inverse_imagebe proven in a way such that they can be moved toFinite_sets? That is, without usingFiniteTornat_unbounded_impl_countably_infinite.This big restructuring of the library comes from some Yak shaving.
homeomorphism,homeomorphicandtopological_property.inverse_mapwould be useful in proofs about it.invertiblein terms ofinverse_map, instead of doing its own thing withInductive.FiniteT.bij_finiteuses something likeeq_cardinal, by redefiningeq_cardinalto useinvertibleas well, we can extract the lemmas ofeq_cardinal _ _from FiniteTypes and state them separately.