begin
:: deftheorem Def1 defines directed WAYBEL_0:def 1 :
:: deftheorem Def2 defines filtered WAYBEL_0:def 2 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem Th5:
:: deftheorem Def3 defines filtered-infs-inheriting WAYBEL_0:def 3 :
:: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def 4 :
theorem
theorem
begin
:: deftheorem defines antitone WAYBEL_0:def 5 :
:: deftheorem Def6 defines directed WAYBEL_0:def 6 :
:: deftheorem defines netmap WAYBEL_0:def 7 :
:: deftheorem defines . WAYBEL_0:def 8 :
:: deftheorem defines monotone WAYBEL_0:def 9 :
:: deftheorem defines antitone WAYBEL_0:def 10 :
:: deftheorem Def11 defines is_eventually_in WAYBEL_0:def 11 :
:: deftheorem defines is_often_in WAYBEL_0:def 12 :
theorem
theorem
theorem
:: deftheorem Def13 defines eventually-directed WAYBEL_0:def 13 :
:: deftheorem Def14 defines eventually-filtered WAYBEL_0:def 14 :
theorem Th11:
theorem Th12:
begin
:: deftheorem Def15 defines downarrow WAYBEL_0:def 15 :
:: deftheorem Def16 defines uparrow WAYBEL_0:def 16 :
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
:: deftheorem defines downarrow WAYBEL_0:def 17 :
:: deftheorem defines uparrow WAYBEL_0:def 18 :
theorem Th17:
theorem Th18:
theorem
theorem
theorem Th21:
theorem Th22:
:: deftheorem Def19 defines lower WAYBEL_0:def 19 :
:: deftheorem Def20 defines upper WAYBEL_0:def 20 :
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
begin
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem
theorem
theorem
:: deftheorem defines principal WAYBEL_0:def 21 :
:: deftheorem defines principal WAYBEL_0:def 22 :
theorem
theorem
:: deftheorem defines Ids WAYBEL_0:def 23 :
:: deftheorem defines Filt WAYBEL_0:def 24 :
:: deftheorem defines Ids_0 WAYBEL_0:def 25 :
:: deftheorem defines Filt_0 WAYBEL_0:def 26 :
definition
let L be non
empty RelStr ;
let X be
Subset of
L;
set D =
{ ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } ;
A1:
{ ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } c= the
carrier of
L
func finsups X -> Subset of
L equals
{ ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } ;
correctness
coherence
{ ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } is Subset of L;
by A1;
set D =
{ ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } ;
A2:
{ ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } c= the
carrier of
L
func fininfs X -> Subset of
L equals
{ ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } ;
correctness
coherence
{ ("/\" Y,L) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L;
by A2;
end;
:: deftheorem defines finsups WAYBEL_0:def 27 :
:: deftheorem defines fininfs WAYBEL_0:def 28 :
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem
theorem
theorem
begin
:: deftheorem Def29 defines connected WAYBEL_0:def 29 :
begin
theorem
theorem
begin
:: deftheorem Def30 defines preserves_inf_of WAYBEL_0:def 30 :
:: deftheorem Def31 defines preserves_sup_of WAYBEL_0:def 31 :
theorem
:: deftheorem defines infs-preserving WAYBEL_0:def 32 :
:: deftheorem defines sups-preserving WAYBEL_0:def 33 :
:: deftheorem defines meet-preserving WAYBEL_0:def 34 :
:: deftheorem defines join-preserving WAYBEL_0:def 35 :
:: deftheorem defines filtered-infs-preserving WAYBEL_0:def 36 :
:: deftheorem defines directed-sups-preserving WAYBEL_0:def 37 :
:: deftheorem Def38 defines isomorphic WAYBEL_0:def 38 :
theorem Th66:
theorem
theorem
theorem Th69:
theorem
theorem
theorem Th72:
theorem
theorem
begin
:: deftheorem Def39 defines up-complete WAYBEL_0:def 39 :
theorem
:: deftheorem Def40 defines /\-complete WAYBEL_0:def 40 :
theorem Th76: