summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2024-05-22Add lemma `filter_setminus_in`adelon
2024-05-22Update label for `genopens`adelon
2024-05-22Update defaulting for envvaradelon
2024-05-22Allow `\left` and `\right` everywhereadelon
2024-05-21Allow line breaks via `\textbox`, handle `\left`/`\right`adelon
2024-05-21Add definition for `\genOpens`adelon
2024-05-21Add simple lemmas on filtersadelon
2024-05-16Attach whitespace info to located tokenadelon
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 Api.hsadelon
2024-05-14Update basis.texadelon
2024-05-07Merge branch 'adelon:main' into mainSimon-Kor
2024-05-07Update noun guessingadelon
2024-05-07Merge branch 'adelon:main' into mainSimon-Kor
2024-05-07formalisation mertic optimizedSimon-Kor
2024-05-07Sketch noun coord, symbols for realsadelon
2024-05-07Sketch lexicon mechanismadelon
2024-05-07Clean up of Notation in numbers.texSimon-Kor
First notation of tupels in the relation set was swapped with the canonical <.
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-30Merge branch 'adelon:main' into mainSimon-Kor
2024-04-30Adding the first formalisation of realsSimon-Kor
2024-04-30Sketch new signature syntaxadelon
2024-04-13first formalisation of addition on naturalsSimon-Kor
We try to Implement the Addition on natural numbers by a relation on N \times N to N such that some of the axioms of the addition holds
2024-04-11Set the Headline Order for the corresponding sectionSimon-Kor
2024-04-11Merge pull request #1 from adelon/mainSimon-Kor
Update Fork
2024-04-11Formalisation of groups and monoidsSimon-Kor
The test.tex file was deleted and all formalisations of groups and monoids was moved to the fitting document of the library. Some proof steps of the new formalisation were optimized for proof time
2024-04-01Allow numbers in markers (from the second char)adelon
2024-03-31Report_in_text_fileSimon-Kor
Txt File Error.txt has been filled
2024-03-31Possible_BugSimon-Kor
In File test.tex line 51 could not be proven, error massage is in the new file error.txt
2024-03-28Merge pull request #1 from Simon-Kor/mainadelon
Allow Windows-style newlines
2024-03-28Allow Windows-style newlinesSimon-Kor
2024-02-10Initial commitadelon