diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-05-07 14:41:15 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-05-07 14:41:15 +0200 |
| commit | 3795588d157864a411baf2fc3afb31f9f5184d93 (patch) | |
| tree | 17e6df25e78c5a1f6453dc64b5b03c0222c91941 /library/set | |
| parent | 937c05e9386dde23432f229e5bc32a1530b26477 (diff) | |
Formalization of metric spaces and some cleaning of numbers.tex
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.
Diffstat (limited to 'library/set')
0 files changed, 0 insertions, 0 deletions