| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-08-12 | way way way more urysohn | Simon-Kor | |
| 2024-08-12 | way way more urysohn | Simon-Kor | |
| 2024-08-12 | way more urysohn | Simon-Kor | |
| 2024-08-12 | Completed the structure of the proof of Urysohn. | Simon-Kor | |
| Now every single step has to be proven. | |||
| 2024-08-12 | more more way more urysohn | Simon-Kor | |
| 2024-08-11 | more more more urysohn | Simon-Kor | |
| 2024-08-10 | more more urysohn | Simon-Kor | |
| 2024-08-10 | more urysohn | Simon-Kor | |
| 2024-08-10 | more ur<sohn | Simon-Kor | |
| 2024-08-09 | put cardinalit to the right place | Simon-Kor | |
| 2024-08-07 | Created first urysohn formalization | Simon-Kor | |
| 2024-06-25 | [Stable] Implented continuous.tex and omitted some proves | Simon-Kor | |
| All changes till here are done such that the check of everything.tex will be a success. There are no logic flaws and false can't be proven with everything out of everthing.tex | |||
| 2024-06-25 | Improvement for the ATP proof time | Simon-Kor | |
| 2024-06-20 | [Stable] Topologgical-space.tex | Simon-Kor | |
| 2024-06-20 | [Report] Task failed and was proven in the same time. | Simon-Kor | |
| The Line 182 has the goal to apply regular in a topological space. But if i try to prove it with Naproche ZF, then the task will be proven and the task fails in the same time. Console Output is the following: time stack exec zf -- --log library/topology/separation.tex -t 30 --dump ./dump [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fx,fB)&subseteq(fB,setminus(s__carrier(fX),fA))&subseteq(setminus(s__carrier(fX),fA),fU)). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,setminus(s__carrier(fX),setminus(s__carrier(fX),fU))=fU). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XN]:(elem(XN,neighbourhoods(fx,fX))&subseteq(XN,fU)&is_closed_in(XN,fX))). [Info] 00:00.21 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,(is_regular(fX)&is_kolmogorov(fX))<=>![XU]:(elem(XU,s__opens(fX))=>![Xx]:(elem(Xx,XU)=>?[XN]:(elem(XN,neighbourhoods(Xx,fX))&subseteq(XN,XU)&is_closed_in(XN,fX))))). [Info] 00:02.34 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))). [Info] 00:02.55 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(fB,setminus(s__carrier(fX),fA))). [Info] 00:08.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,closeds(fX))&elem(fx,fN)&subseteq(fN,fU)). [Info] 00:10.70 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(setminus(s__carrier(fX),fA),setminus(s__carrier(fX),setminus(s__carrier(fX),fU)))). [Info] 00:10.98 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,neighbourhoods(fx,fX))). Verification failed: prover found countermodel fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))).fof(is_regular,axiom,![XX]:(is_regular(XX)<=>![XV]:![Xp,XC]:((elem(Xp,s__carrier(XX))&~elem(Xp,XC)&elem(XC,closeds(XX)))=>?[XU,XC]:(elem(XU,s__opens(XX))&elem(XC,s__opens(XX))&elem(Xp,XU)&subseteq(XC,XV)&inter(XU,XV)=emptyset)))). fof(eqvilance_teethree_closed_neighbourhood_in_open1,axiom,elem(fx,s__carrier(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open2,axiom,~elem(fx,fC)). fof(eqvilance_teethree_closed_neighbourhood_in_open3,axiom,elem(fC,closeds(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open4,axiom,fC=setminus(s__carrier(fX),fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open5,axiom,elem(fx,fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open6,axiom,elem(fU,s__opens(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open7,axiom,is_regular(fX)&is_kolmogorov(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open8,axiom,inhabited(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open9,axiom,topological_space(fX)). real 0m14.914s user 0m37.867s sys 0m1.956s | |||
| 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-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 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 | 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-22 | Update label for `genopens` | adelon | |
| 2024-05-21 | Allow line breaks via `\textbox`, handle `\left`/`\right` | 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 basis.tex | adelon | |
| 2024-05-07 | formalisation mertic optimized | Simon-Kor | |
| 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 | Adding the first formalisation of reals | Simon-Kor | |
| 2024-02-10 | Initial commit | adelon | |
 |
index : naproche-zf.git | |
| Unnamed repository; edit this file 'description' to name the repository. |
| summaryrefslogtreecommitdiff |