felix.git/library/topology/order-topology.tex, branch hotgUnnamed repository; edit this file 'description' to name the repository.
https://git.adelon.net/felix.git/atom?h=hotg2024-05-07T12:41:15+00:00Formalization of metric spaces and some cleaning of numbers.tex2024-05-07T12:41:15+00:00Simon-Kor52245124+Simon-Kor@users.noreply.github.com2024-05-07T12:41:15+00:00urn:sha1:3795588d157864a411baf2fc3afb31f9f5184d93
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.
Adding the first formalisation of reals2024-04-30T10:26:13+00:00Simon-Kor52245124+Simon-Kor@users.noreply.github.com2024-04-30T10:26:13+00:00urn:sha1:cfd5061ced34f061e84ecca2a266f8f4cd01ce36