|
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
|
