| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-06-18 | Merge remote-tracking branch 'upstream/main' | Simon-Kor | |
| 2024-06-18 | Definition of T3 and regular spaces. | Simon-Kor | |
| 2024-06-18 | Update topological-space.tex | adelon | |
| 2024-06-17 | Completed proofs [stable] | Simon-Kor | |
| 2024-06-16 | First implementation of basic relations of closed and open. | Simon-Kor | |
| Not finished. | |||
| 2024-06-12 | Prove Bug "Ex falso quodlibet" | Simon-Kor | |
| The generated ATP Tasks are done in few secounds, if they are send manually to Vampire. But if its done in Naproche all together it won't work. | |||
| 2024-06-11 | proof of complement_interior_eq_closure_complement and some more about ↵ | Simon-Kor | |
| clousures(unsatable) | |||
| 2024-06-10 | Dedupe helper function | adelon | |
| 2024-06-05 | Update Megalodon.hs | adelon | |
| 2024-06-04 | Proof of teetwo_space_is_teeone_space | Simon-Kor | |
| 2024-06-04 | Proof of teeone_implies_singletons_closed | Simon-Kor | |
| The Assumption was changed, for usage of bounded variables. Maybe there is a bug with Omitted. Omitted restricts the Ambigus Phrase testing. | |||
| 2024-06-04 | Some notation fixes and lemma for topo basis generats opens was proofed and ↵ | Simon-Kor | |
| optimizised | |||
| 2024-05-28 | Merge pull request #2 from adelon/main | Simon-Kor | |
| changes from main needs to be included | |||
| 2024-05-28 | Merge branch 'main' into main | Simon-Kor | |
| 2024-05-28 | unexpected behavior of vampire | Simon-Kor | |
| The task topological behavior is proofed in seconds by just vampire, but with mode casc it takes plenty seconds | |||
| 2024-05-28 | Update `inters_in_genopens` | adelon | |
| 2024-05-28 | Pow closed under binary intersection | adelon | |
| 2024-05-28 | Merge branch 'main' into main | Simon-Kor | |
| 2024-05-28 | proofing some lammes about topological basis | Simon-Kor | |
| 2024-05-25 | Prove `emptyset_open` to replace structure axiom | adelon | |
| 2024-05-23 | Update formatting | adelon | |
| 2024-05-22 | Update filter.tex | adelon | |
| 2024-05-22 | Add filter lemmas | adelon | |
| 2024-05-22 | Add lemma `filter_setminus_in` | adelon | |
| 2024-05-22 | Update label for `genopens` | adelon | |
| 2024-05-22 | Update defaulting for envvar | adelon | |
| 2024-05-22 | Allow `\left` and `\right` everywhere | adelon | |
| 2024-05-21 | Allow line breaks via `\textbox`, handle `\left`/`\right` | adelon | |
| 2024-05-21 | Add definition for `\genOpens` | adelon | |
| 2024-05-21 | Add simple lemmas on filters | adelon | |
| 2024-05-16 | Attach whitespace info to located token | adelon | |
| 2024-05-16 | Fix missing `\text` | adelon | |
| 2024-05-14 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-05-14 | work on metric spaces | Simon-Kor | |
| 2024-05-14 | Update Api.hs | adelon | |
| 2024-05-14 | Update basis.tex | adelon | |
| 2024-05-07 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-05-07 | Update noun guessing | adelon | |
| 2024-05-07 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-05-07 | formalisation mertic optimized | Simon-Kor | |
| 2024-05-07 | Sketch noun coord, symbols for reals | adelon | |
| 2024-05-07 | Sketch lexicon mechanism | adelon | |
| 2024-05-07 | Clean up of Notation in numbers.tex | Simon-Kor | |
| First notation of tupels in the relation set was swapped with the canonical <. | |||
| 2024-05-07 | Formalization of metric spaces and some cleaning of numbers.tex | Simon-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-30 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-04-30 | Adding the first formalisation of reals | Simon-Kor | |
| 2024-04-30 | Sketch new signature syntax | adelon | |
| 2024-04-13 | first formalisation of addition on naturals | Simon-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-11 | Set the Headline Order for the corresponding section | Simon-Kor | |
| 2024-04-11 | Merge pull request #1 from adelon/main | Simon-Kor | |
| Update Fork | |||
 |
index : naproche-zf.git | |
| Unnamed repository; edit this file 'description' to name the repository. |
| summaryrefslogtreecommitdiff |