summaryrefslogtreecommitdiff
path: root/library/topology/metric-space.tex
AgeCommit message (Collapse)Author
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.