summaryrefslogtreecommitdiff
path: root/library/topology/metric-space.tex
AgeCommit message (Collapse)Author
2024-09-15Issue at Fixing.Simon-Kor
In Line 49 in real-topological-space.tex the Fix can't be processed.
2024-06-04Some notation fixes and lemma for topo basis generats opens was proofed and ↵Simon-Kor
optimizised
2024-05-28proofing some lammes about topological basisSimon-Kor
2024-05-14work on metric spacesSimon-Kor
2024-05-07formalisation mertic optimizedSimon-Kor
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.