summaryrefslogtreecommitdiff
path: root/library/numbers.tex
AgeCommit message (Collapse)Author
2024-07-06Formalisation of integers.Simon-Kor
2024-07-06Finished the formalization of naturals.Simon-Kor
2024-07-05Proof of 1 is identity on the naturals and beginSimon-Kor
of Disstributiv law naturals proof
2024-07-02Further Formalisation of naturals.Simon-Kor
Such as induction on naturals and addition laws.
2024-07-02Definition and axioms of naturals.Simon-Kor
2024-06-26Working at the numbers.texSimon-Kor
2024-06-25Sorted the structure of numbers.texSimon-Kor
2024-06-04Some notation fixes and lemma for topo basis generats opens was proofed and ↵Simon-Kor
optimizised
2024-05-14work on metric spacesSimon-Kor
2024-05-07formalisation mertic optimizedSimon-Kor
2024-05-07Clean up of Notation in numbers.texSimon-Kor
First notation of tupels in the relation set was swapped with the canonical <.
2024-05-07Formalization of metric spaces and some cleaning of numbers.texSimon-Kor
Formalization of metric spaces: Therefore we introduced the predicate metric and its axiomatization. Then we introduced the term metric space in dependence of a metric function. This metric space is automatically a a topological space.
2024-04-30Adding the first formalisation of realsSimon-Kor