summaryrefslogtreecommitdiff
path: root/library/topology
AgeCommit message (Collapse)Author
2024-05-28Update `inters_in_genopens`adelon
2024-05-28Merge branch 'main' into mainSimon-Kor
2024-05-28proofing some lammes about topological basisSimon-Kor
2024-05-25Prove `emptyset_open` to replace structure axiomadelon
2024-05-22Update label for `genopens`adelon
2024-05-21Allow line breaks via `\textbox`, handle `\left`/`\right`adelon
2024-05-16Fix missing `\text`adelon
2024-05-14Merge branch 'adelon:main' into mainSimon-Kor
2024-05-14work on metric spacesSimon-Kor
2024-05-14Update basis.texadelon
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.
2024-04-30Adding the first formalisation of realsSimon-Kor
2024-02-10Initial commitadelon