:: by Robert Milewski

::

:: Received December 1, 1996

:: Copyright (c) 1996-2021 Association of Mizar Users

definition

let L be non empty reflexive RelStr ;

ex b_{1} being strict full SubRelStr of L st

for x being Element of L holds

( x in the carrier of b_{1} iff x is compact )

for b_{1}, b_{2} being strict full SubRelStr of L st ( for x being Element of L holds

( x in the carrier of b_{1} iff x is compact ) ) & ( for x being Element of L holds

( x in the carrier of b_{2} iff x is compact ) ) holds

b_{1} = b_{2}

end;
func CompactSublatt L -> strict full SubRelStr of L means :Def1: :: WAYBEL_8:def 1

for x being Element of L holds

( x in the carrier of it iff x is compact );

existence for x being Element of L holds

( x in the carrier of it iff x is compact );

ex b

for x being Element of L holds

( x in the carrier of b

proof end;

uniqueness for b

( x in the carrier of b

( x in the carrier of b

b

proof end;

:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def 1 :

for L being non empty reflexive RelStr

for b_{2} being strict full SubRelStr of L holds

( b_{2} = CompactSublatt L iff for x being Element of L holds

( x in the carrier of b_{2} iff x is compact ) );

for L being non empty reflexive RelStr

for b

( b

( x in the carrier of b

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;

coherence

not CompactSublatt L is empty

end;
coherence

not CompactSublatt L is empty

proof end;

theorem :: WAYBEL_8:1

for L being complete LATTICE

for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds

x << y

for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds

x << y

proof end;

theorem :: WAYBEL_8:2

for L being complete LATTICE

for x being Element of L holds

( uparrow x is Open Filter of L iff x is compact )

for x being Element of L holds

( uparrow x is Open Filter of L iff x is compact )

proof end;

theorem :: WAYBEL_8:3

for L being non empty with_suprema lower-bounded Poset holds

( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )

( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )

proof end;

definition

let L be non empty reflexive RelStr ;

let x be Element of L;

{ y where y is Element of L : ( x >= y & y is compact ) } is Subset of L

end;
let x be Element of L;

func compactbelow x -> Subset of L equals :: WAYBEL_8:def 2

{ y where y is Element of L : ( x >= y & y is compact ) } ;

coherence { y where y is Element of L : ( x >= y & y is compact ) } ;

{ y where y is Element of L : ( x >= y & y is compact ) } is Subset of L

proof end;

:: deftheorem defines compactbelow WAYBEL_8:def 2 :

for L being non empty reflexive RelStr

for x being Element of L holds compactbelow x = { y where y is Element of L : ( x >= y & y is compact ) } ;

for L being non empty reflexive RelStr

for x being Element of L holds compactbelow x = { y where y is Element of L : ( x >= y & y is compact ) } ;

theorem Th4: :: WAYBEL_8:4

for L being non empty reflexive RelStr

for x, y being Element of L holds

( y in compactbelow x iff ( x >= y & y is compact ) )

for x, y being Element of L holds

( y in compactbelow x iff ( x >= y & y is compact ) )

proof end;

theorem Th5: :: WAYBEL_8:5

for L being non empty reflexive RelStr

for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)

for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)

proof end;

theorem Th6: :: WAYBEL_8:6

for L being non empty reflexive transitive RelStr

for x being Element of L holds compactbelow x c= waybelow x

for x being Element of L holds compactbelow x c= waybelow x

proof end;

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;

let x be Element of L;

coherence

not compactbelow x is empty

end;
let x be Element of L;

coherence

not compactbelow x is empty

proof end;

definition

let L be non empty reflexive RelStr ;

end;
attr L is satisfying_axiom_K means :Def3: :: WAYBEL_8:def 3

for x being Element of L holds x = sup (compactbelow x);

for x being Element of L holds x = sup (compactbelow x);

:: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def 3 :

for L being non empty reflexive RelStr holds

( L is satisfying_axiom_K iff for x being Element of L holds x = sup (compactbelow x) );

for L being non empty reflexive RelStr holds

( L is satisfying_axiom_K iff for x being Element of L holds x = sup (compactbelow x) );

definition

let L be non empty reflexive RelStr ;

end;
attr L is algebraic means :Def4: :: WAYBEL_8:def 4

( ( for x being Element of L holds

( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K );

( ( for x being Element of L holds

( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K );

:: deftheorem Def4 defines algebraic WAYBEL_8:def 4 :

for L being non empty reflexive RelStr holds

( L is algebraic iff ( ( for x being Element of L holds

( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ) );

for L being non empty reflexive RelStr holds

( L is algebraic iff ( ( for x being Element of L holds

( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ) );

theorem Th7: :: WAYBEL_8:7

for L being LATTICE holds

( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds

ex k being Element of L st

( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )

( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds

ex k being Element of L st

( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )

proof end;

registration

for b_{1} being LATTICE st b_{1} is algebraic holds

b_{1} is continuous
by Th7;

end;

cluster reflexive transitive antisymmetric with_suprema with_infima algebraic -> continuous for RelStr ;

coherence for b

b

registration

for b_{1} being non empty reflexive RelStr st b_{1} is algebraic holds

( b_{1} is up-complete & b_{1} is satisfying_axiom_K )
;

end;

cluster non empty reflexive algebraic -> non empty reflexive up-complete satisfying_axiom_K for RelStr ;

coherence for b

( b

registration
end;

definition

let L be non empty reflexive RelStr ;

end;
attr L is arithmetic means :: WAYBEL_8:def 5

( L is algebraic & CompactSublatt L is meet-inheriting );

( L is algebraic & CompactSublatt L is meet-inheriting );

:: deftheorem defines arithmetic WAYBEL_8:def 5 :

for L being non empty reflexive RelStr holds

( L is arithmetic iff ( L is algebraic & CompactSublatt L is meet-inheriting ) );

for L being non empty reflexive RelStr holds

( L is arithmetic iff ( L is algebraic & CompactSublatt L is meet-inheriting ) );

registration

for b_{1} being LATTICE st b_{1} is arithmetic holds

b_{1} is algebraic
;

end;

cluster reflexive transitive antisymmetric with_suprema with_infima arithmetic -> algebraic for RelStr ;

coherence for b

b

registration

for b_{1} being LATTICE st b_{1} is trivial holds

b_{1} is arithmetic
end;

cluster trivial reflexive transitive antisymmetric with_suprema with_infima -> arithmetic for RelStr ;

coherence for b

b

proof end;

registration

ex b_{1} being LATTICE st

( b_{1} is 1 -element & b_{1} is strict )
end;

cluster non empty 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ;

existence ex b

( b

proof end;

theorem Th8: :: WAYBEL_8:8

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds

for x1, y1 being Element of L1

for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds

x2 << y2

for x1, y1 being Element of L1

for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds

x2 << y2

proof end;

theorem Th9: :: WAYBEL_8:9

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds

for x being Element of L1

for y being Element of L2 st x = y & x is compact holds

y is compact

for x being Element of L1

for y being Element of L2 st x = y & x is compact holds

y is compact

proof end;

theorem Th10: :: WAYBEL_8:10

for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds

for x being Element of L1

for y being Element of L2 st x = y holds

compactbelow x = compactbelow y

for x being Element of L1

for y being Element of L2 st x = y holds

compactbelow x = compactbelow y

proof end;

theorem :: WAYBEL_8:11

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & not L1 is empty holds

not L2 is empty ;

not L2 is empty ;

theorem Th12: :: WAYBEL_8:12

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive holds

L2 is reflexive ;

L2 is reflexive ;

theorem Th13: :: WAYBEL_8:13

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive holds

L2 is transitive ;

L2 is transitive ;

theorem Th14: :: WAYBEL_8:14

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric holds

L2 is antisymmetric ;

L2 is antisymmetric ;

theorem Th15: :: WAYBEL_8:15

for L1, L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds

L2 is up-complete

L2 is up-complete

proof end;

theorem Th16: :: WAYBEL_8:16

for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds

( not compactbelow x is empty & compactbelow x is directed ) ) holds

L2 is satisfying_axiom_K

( not compactbelow x is empty & compactbelow x is directed ) ) holds

L2 is satisfying_axiom_K

proof end;

theorem Th17: :: WAYBEL_8:17

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic holds

L2 is algebraic

L2 is algebraic

proof end;

theorem Th18: :: WAYBEL_8:18

for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic holds

L2 is arithmetic

L2 is arithmetic

proof end;

registration

let L be non empty RelStr ;

coherence

not RelStr(# the carrier of L, the InternalRel of L #) is empty ;

end;
coherence

not RelStr(# the carrier of L, the InternalRel of L #) is empty ;

registration

let L be non empty reflexive RelStr ;

coherence

RelStr(# the carrier of L, the InternalRel of L #) is reflexive by Th12;

end;
coherence

RelStr(# the carrier of L, the InternalRel of L #) is reflexive by Th12;

registration

let L be transitive RelStr ;

coherence

RelStr(# the carrier of L, the InternalRel of L #) is transitive by Th13;

end;
coherence

RelStr(# the carrier of L, the InternalRel of L #) is transitive by Th13;

registration

let L be antisymmetric RelStr ;

coherence

RelStr(# the carrier of L, the InternalRel of L #) is antisymmetric by Th14;

end;
coherence

RelStr(# the carrier of L, the InternalRel of L #) is antisymmetric by Th14;

registration

let L be with_infima RelStr ;

coherence

RelStr(# the carrier of L, the InternalRel of L #) is with_infima by YELLOW_7:14;

end;
coherence

RelStr(# the carrier of L, the InternalRel of L #) is with_infima by YELLOW_7:14;

registration

let L be with_suprema RelStr ;

coherence

RelStr(# the carrier of L, the InternalRel of L #) is with_suprema by YELLOW_7:15;

end;
coherence

RelStr(# the carrier of L, the InternalRel of L #) is with_suprema by YELLOW_7:15;

registration

let L be non empty reflexive up-complete RelStr ;

coherence

RelStr(# the carrier of L, the InternalRel of L #) is up-complete by Th15;

end;
coherence

RelStr(# the carrier of L, the InternalRel of L #) is up-complete by Th15;

registration

let L be non empty reflexive antisymmetric algebraic RelStr ;

coherence

RelStr(# the carrier of L, the InternalRel of L #) is algebraic by Th17;

end;
coherence

RelStr(# the carrier of L, the InternalRel of L #) is algebraic by Th17;

registration

let L be arithmetic LATTICE;

coherence

RelStr(# the carrier of L, the InternalRel of L #) is arithmetic by Th18;

end;
coherence

RelStr(# the carrier of L, the InternalRel of L #) is arithmetic by Th18;

theorem Th20: :: WAYBEL_8:20

for L being lower-bounded algebraic LATTICE holds

( L is arithmetic iff L -waybelow is multiplicative )

( L is arithmetic iff L -waybelow is multiplicative )

proof end;

theorem :: WAYBEL_8:21

for L being lower-bounded arithmetic LATTICE

for p being Element of L st p is pseudoprime holds

p is prime

for p being Element of L st p is pseudoprime holds

p is prime

proof end;

theorem :: WAYBEL_8:22

for L being lower-bounded distributive algebraic LATTICE st ( for p being Element of L st p is pseudoprime holds

p is prime ) holds

L is arithmetic

p is prime ) holds

L is arithmetic

proof end;

registration

let L be algebraic LATTICE;

let c be closure Function of L,L;

existence

ex b_{1} being Subset of (Image c) st

( not b_{1} is empty & b_{1} is directed )

end;
let c be closure Function of L,L;

existence

ex b

( not b

proof end;

theorem Th23: :: WAYBEL_8:23

for L being algebraic LATTICE

for c being closure Function of L,L st c is directed-sups-preserving holds

c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))

for c being closure Function of L,L st c is directed-sups-preserving holds

c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))

proof end;

theorem :: WAYBEL_8:24

for L being lower-bounded algebraic LATTICE

for c being closure Function of L,L st c is directed-sups-preserving holds

Image c is algebraic LATTICE

for c being closure Function of L,L st c is directed-sups-preserving holds

Image c is algebraic LATTICE

proof end;

theorem :: WAYBEL_8:25

for L being lower-bounded algebraic LATTICE

for c being closure Function of L,L st c is directed-sups-preserving holds

c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))

for c being closure Function of L,L st c is directed-sups-preserving holds

c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))

proof end;

theorem Th27: :: WAYBEL_8:27

for X being set

for x, y being Element of (BoolePoset X) holds

( x << y iff for Y being Subset-Family of X st y c= union Y holds

ex Z being finite Subset of Y st x c= union Z )

for x, y being Element of (BoolePoset X) holds

( x << y iff for Y being Subset-Family of X st y c= union Y holds

ex Z being finite Subset of Y st x c= union Z )

proof end;

theorem Th29: :: WAYBEL_8:29

for X being set

for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum }

for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum }

proof end;

theorem :: WAYBEL_8:30

for X being set

for F being Subset of X holds

( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )

for F being Subset of X holds

( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )

proof end;

registration

let X be set ;

let x be Element of (BoolePoset X);

coherence

( compactbelow x is lower & compactbelow x is directed )

end;
let x be Element of (BoolePoset X);

coherence

( compactbelow x is lower & compactbelow x is directed )

proof end;

registration
end;