:: by Grzegorz Bancerek

::

:: Received December 1, 1996

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

begin

theorem Th1: :: WAYBEL_7:1

for L being complete LATTICE

for X, Y being set st X c= Y holds

( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) )

for X, Y being set st X c= Y holds

( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) )

proof end;

registration
end;

theorem Th4: :: WAYBEL_7:4

for L being non empty lower-bounded Poset

for F being Filter of L holds

( F is proper iff not Bottom L in F )

for F being Filter of L holds

( F is proper iff not Bottom L in F )

proof end;

registration

ex b_{1} being LATTICE st

( not b_{1} is trivial & b_{1} is Boolean & b_{1} is strict )
end;

cluster non empty non trivial strict reflexive transitive antisymmetric Boolean non void with_suprema with_infima for RelStr ;

existence ex b

( not b

proof end;

registration

let L be non trivial upper-bounded Poset;

existence

ex b_{1} being Filter of L st b_{1} is proper

end;
existence

ex b

proof end;

theorem :: WAYBEL_7:6

for X being set

for Y being Subset of (BoolePoset X) holds

( Y is lower iff for x, y being set st x c= y & y in Y holds

x in Y )

for Y being Subset of (BoolePoset X) holds

( Y is lower iff for x, y being set st x c= y & y in Y holds

x in Y )

proof end;

theorem Th7: :: WAYBEL_7:7

for X being set

for Y being Subset of (BoolePoset X) holds

( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds

y in Y )

for Y being Subset of (BoolePoset X) holds

( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds

y in Y )

proof end;

theorem :: WAYBEL_7:8

for X being set

for Y being lower Subset of (BoolePoset X) holds

( Y is directed iff for x, y being set st x in Y & y in Y holds

x \/ y in Y )

for Y being lower Subset of (BoolePoset X) holds

( Y is directed iff for x, y being set st x in Y & y in Y holds

x \/ y in Y )

proof end;

theorem Th9: :: WAYBEL_7:9

for X being set

for Y being upper Subset of (BoolePoset X) holds

( Y is filtered iff for x, y being set st x in Y & y in Y holds

x /\ y in Y )

for Y being upper Subset of (BoolePoset X) holds

( Y is filtered iff for x, y being set st x in Y & y in Y holds

x /\ y in Y )

proof end;

theorem :: WAYBEL_7:10

for X being set

for Y being non empty lower Subset of (BoolePoset X) holds

( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds

union Z in Y )

for Y being non empty lower Subset of (BoolePoset X) holds

( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds

union Z in Y )

proof end;

theorem Th11: :: WAYBEL_7:11

for X being set

for Y being non empty upper Subset of (BoolePoset X) holds

( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds

Intersect Z in Y )

for Y being non empty upper Subset of (BoolePoset X) holds

( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds

Intersect Z in Y )

proof end;

begin

:: deftheorem Def1 defines prime WAYBEL_7:def 1 :

for L being with_infima Poset

for I being Ideal of L holds

( I is prime iff for x, y being Element of L holds

( not x "/\" y in I or x in I or y in I ) );

for L being with_infima Poset

for I being Ideal of L holds

( I is prime iff for x, y being Element of L holds

( not x "/\" y in I or x in I or y in I ) );

theorem Th12: :: WAYBEL_7:12

for L being with_infima Poset

for I being Ideal of L holds

( I is prime iff for A being non empty finite Subset of L st inf A in I holds

ex a being Element of L st

( a in A & a in I ) )

for I being Ideal of L holds

( I is prime iff for A being non empty finite Subset of L st inf A in I holds

ex a being Element of L st

( a in A & a in I ) )

proof end;

registration
end;

theorem :: WAYBEL_7:13

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

for x being set st x is prime Ideal of L1 holds

x is prime Ideal of L2

for x being set st x is prime Ideal of L1 holds

x is prime Ideal of L2

proof end;

:: deftheorem Def2 defines prime WAYBEL_7:def 2 :

for L being with_suprema Poset

for F being Filter of L holds

( F is prime iff for x, y being Element of L holds

( not x "\/" y in F or x in F or y in F ) );

for L being with_suprema Poset

for F being Filter of L holds

( F is prime iff for x, y being Element of L holds

( not x "\/" y in F or x in F or y in F ) );

theorem :: WAYBEL_7:14

for L being with_suprema Poset

for F being Filter of L holds

( F is prime iff for A being non empty finite Subset of L st sup A in F holds

ex a being Element of L st

( a in A & a in F ) )

for F being Filter of L holds

( F is prime iff for A being non empty finite Subset of L st sup A in F holds

ex a being Element of L st

( a in A & a in F ) )

proof end;

registration
end;

theorem Th15: :: WAYBEL_7:15

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

for x being set st x is prime Filter of L1 holds

x is prime Filter of L2

for x being set st x is prime Filter of L1 holds

x is prime Filter of L2

proof end;

theorem Th16: :: WAYBEL_7:16

for L being LATTICE

for x being set holds

( x is prime Ideal of L iff x is prime Filter of (L opp) )

for x being set holds

( x is prime Ideal of L iff x is prime Filter of (L opp) )

proof end;

theorem Th17: :: WAYBEL_7:17

for L being LATTICE

for x being set holds

( x is prime Filter of L iff x is prime Ideal of (L opp) )

for x being set holds

( x is prime Filter of L iff x is prime Ideal of (L opp) )

proof end;

:: Remark 3.16: (3) iff (2)

theorem :: WAYBEL_7:18

for L being with_infima Poset

for I being Ideal of L holds

( I is prime iff ( I ` is Filter of L or I ` = {} ) )

for I being Ideal of L holds

( I is prime iff ( I ` is Filter of L or I ` = {} ) )

proof end;

:: Remark 3.16: (3) iff (1)

theorem Th20: :: WAYBEL_7:20

for L being Boolean LATTICE

for F being Filter of L holds

( F is prime iff for a being Element of L holds

( a in F or 'not' a in F ) )

for F being Filter of L holds

( F is prime iff for a being Element of L holds

( a in F or 'not' a in F ) )

proof end;

:: Remark 3.18: (1) iff (2)

theorem Th21: :: WAYBEL_7:21

for X being set

for F being Filter of (BoolePoset X) holds

( F is prime iff for A being Subset of X holds

( A in F or X \ A in F ) )

for F being Filter of (BoolePoset X) holds

( F is prime iff for A being Subset of X holds

( A in F or X \ A in F ) )

proof end;

:: deftheorem Def3 defines ultra WAYBEL_7:def 3 :

for L being non empty Poset

for F being Filter of L holds

( F is ultra iff ( F is proper & ( for G being Filter of L holds

( not F c= G or F = G or G = the carrier of L ) ) ) );

for L being non empty Poset

for F being Filter of L holds

( F is ultra iff ( F is proper & ( for G being Filter of L holds

( not F c= G or F = G or G = the carrier of L ) ) ) );

registration

let L be non empty Poset;

coherence

for b_{1} being Filter of L st b_{1} is ultra holds

b_{1} is proper
by Def3;

end;
coherence

for b

b

Lm1: for L being with_infima Poset

for F being Filter of L

for X being non empty finite Subset of L

for x being Element of L st x in uparrow (fininfs (F \/ X)) holds

ex a being Element of L st

( a in F & x >= a "/\" (inf X) )

proof end;

:: Remark 3.18: (1)+proper iff (3)

theorem Th22: :: WAYBEL_7:22

for L being Boolean LATTICE

for F being Filter of L holds

( ( F is proper & F is prime ) iff F is ultra )

for F being Filter of L holds

( ( F is proper & F is prime ) iff F is ultra )

proof end;

Lm2: for L being with_suprema Poset

for I being Ideal of L

for X being non empty finite Subset of L

for x being Element of L st x in downarrow (finsups (I \/ X)) holds

ex i being Element of L st

( i in I & x <= i "\/" (sup X) )

proof end;

:: Lemma 3.19

theorem Th23: :: WAYBEL_7:23

for L being distributive LATTICE

for I being Ideal of L

for F being Filter of L st I misses F holds

ex P being Ideal of L st

( P is prime & I c= P & P misses F )

for I being Ideal of L

for F being Filter of L st I misses F holds

ex P being Ideal of L st

( P is prime & I c= P & P misses F )

proof end;

theorem Th24: :: WAYBEL_7:24

for L being distributive LATTICE

for I being Ideal of L

for x being Element of L st not x in I holds

ex P being Ideal of L st

( P is prime & I c= P & not x in P )

for I being Ideal of L

for x being Element of L st not x in I holds

ex P being Ideal of L st

( P is prime & I c= P & not x in P )

proof end;

theorem Th25: :: WAYBEL_7:25

for L being distributive LATTICE

for I being Ideal of L

for F being Filter of L st I misses F holds

ex P being Filter of L st

( P is prime & F c= P & I misses P )

for I being Ideal of L

for F being Filter of L st I misses F holds

ex P being Filter of L st

( P is prime & F c= P & I misses P )

proof end;

theorem Th26: :: WAYBEL_7:26

for L being non trivial Boolean LATTICE

for F being proper Filter of L ex G being Filter of L st

( F c= G & G is ultra )

for F being proper Filter of L ex G being Filter of L st

( F c= G & G is ultra )

proof end;

begin

definition

let T be TopSpace;

let F, x be set ;

end;
let F, x be set ;

pred x is_a_cluster_point_of F,T means :Def4: :: WAYBEL_7:def 4

for A being Subset of T st A is open & x in A holds

for B being set st B in F holds

A meets B;

for A being Subset of T st A is open & x in A holds

for B being set st B in F holds

A meets B;

pred x is_a_convergence_point_of F,T means :Def5: :: WAYBEL_7:def 5

for A being Subset of T st A is open & x in A holds

A in F;

for A being Subset of T st A is open & x in A holds

A in F;

:: deftheorem Def4 defines is_a_cluster_point_of WAYBEL_7:def 4 :

for T being TopSpace

for F, x being set holds

( x is_a_cluster_point_of F,T iff for A being Subset of T st A is open & x in A holds

for B being set st B in F holds

A meets B );

for T being TopSpace

for F, x being set holds

( x is_a_cluster_point_of F,T iff for A being Subset of T st A is open & x in A holds

for B being set st B in F holds

A meets B );

:: deftheorem Def5 defines is_a_convergence_point_of WAYBEL_7:def 5 :

for T being TopSpace

for F, x being set holds

( x is_a_convergence_point_of F,T iff for A being Subset of T st A is open & x in A holds

A in F );

for T being TopSpace

for F, x being set holds

( x is_a_convergence_point_of F,T iff for A being Subset of T st A is open & x in A holds

A in F );

registration

let X be non empty set ;

existence

ex b_{1} being Filter of (BoolePoset X) st b_{1} is ultra

end;
existence

ex b

proof end;

theorem Th27: :: WAYBEL_7:27

for T being non empty TopSpace

for F being ultra Filter of (BoolePoset the carrier of T)

for p being set holds

( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )

for F being ultra Filter of (BoolePoset the carrier of T)

for p being set holds

( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )

proof end;

:: Proposition 3.20 (1) => (2)

theorem Th28: :: WAYBEL_7:28

for T being non empty TopSpace

for x, y being Element of (InclPoset the topology of T) st x << y holds

for F being proper Filter of (BoolePoset the carrier of T) st x in F holds

ex p being Element of T st

( p in y & p is_a_cluster_point_of F,T )

for x, y being Element of (InclPoset the topology of T) st x << y holds

for F being proper Filter of (BoolePoset the carrier of T) st x in F holds

ex p being Element of T st

( p in y & p is_a_cluster_point_of F,T )

proof end;

:: Proposition 3.20: (1) => (3)

theorem :: WAYBEL_7:29

for T being non empty TopSpace

for x, y being Element of (InclPoset the topology of T) st x << y holds

for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds

ex p being Element of T st

( p in y & p is_a_convergence_point_of F,T )

for x, y being Element of (InclPoset the topology of T) st x << y holds

for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds

ex p being Element of T st

( p in y & p is_a_convergence_point_of F,T )

proof end;

:: Proposition 3.20: (3) => (1)

theorem Th30: :: WAYBEL_7:30

for T being non empty TopSpace

for x, y being Element of (InclPoset the topology of T) st x c= y & ( for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds

ex p being Element of T st

( p in y & p is_a_convergence_point_of F,T ) ) holds

x << y

for x, y being Element of (InclPoset the topology of T) st x c= y & ( for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds

ex p being Element of T st

( p in y & p is_a_convergence_point_of F,T ) ) holds

x << y

proof end;

theorem :: WAYBEL_7:31

for T being non empty TopSpace

for B being prebasis of T

for x, y being Element of (InclPoset the topology of T) st x c= y holds

( x << y iff for F being Subset of B st y c= union F holds

ex G being finite Subset of F st x c= union G )

for B being prebasis of T

for x, y being Element of (InclPoset the topology of T) st x c= y holds

( x << y iff for F being Subset of B st y c= union F holds

ex G being finite Subset of F st x c= union G )

proof end;

:: Proposition 3.22

theorem :: WAYBEL_7:32

for L being distributive complete LATTICE

for x, y being Element of L holds

( x << y iff for P being prime Ideal of L st y <= sup P holds

x in P )

for x, y being Element of L holds

( x << y iff for P being prime Ideal of L st y <= sup P holds

x in P )

proof end;

begin

:: deftheorem Def6 defines pseudoprime WAYBEL_7:def 6 :

for L being LATTICE

for p being Element of L holds

( p is pseudoprime iff ex P being prime Ideal of L st p = sup P );

for L being LATTICE

for p being Element of L holds

( p is pseudoprime iff ex P being prime Ideal of L st p = sup P );

:: Proposition 3.24: (1) => (2)

theorem Th35: :: WAYBEL_7:35

for L being continuous LATTICE

for p being Element of L st p is pseudoprime holds

for A being non empty finite Subset of L st inf A << p holds

ex a being Element of L st

( a in A & a <= p )

for p being Element of L st p is pseudoprime holds

for A being non empty finite Subset of L st inf A << p holds

ex a being Element of L st

( a in A & a <= p )

proof end;

:: Proposition 3.24: (2)+? => (3)

theorem :: WAYBEL_7:36

for L being continuous LATTICE

for p being Element of L st ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds

ex a being Element of L st

( a in A & a <= p ) ) holds

uparrow (fininfs ((downarrow p) `)) misses waybelow p

for p being Element of L st ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds

ex a being Element of L st

( a in A & a <= p ) ) holds

uparrow (fininfs ((downarrow p) `)) misses waybelow p

proof end;

:: It is not true that: Proposition 3.24: (2) => (3)

theorem :: WAYBEL_7:37

for L being continuous LATTICE st Top L is compact holds

( ( for A being non empty finite Subset of L st inf A << Top L holds

ex a being Element of L st

( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) )

( ( for A being non empty finite Subset of L st inf A << Top L holds

ex a being Element of L st

( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) )

proof end;

:: Proposition 3.24: (2) <= (3)

theorem :: WAYBEL_7:38

for L being continuous LATTICE

for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds

for A being non empty finite Subset of L st inf A << p holds

ex a being Element of L st

( a in A & a <= p )

for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds

for A being non empty finite Subset of L st inf A << p holds

ex a being Element of L st

( a in A & a <= p )

proof end;

:: Proposition 3.24: (3) => (1)

theorem :: WAYBEL_7:39

for L being distributive continuous LATTICE

for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds

p is pseudoprime

for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds

p is pseudoprime

proof end;

:: deftheorem Def7 defines multiplicative WAYBEL_7:def 7 :

for L being non empty RelStr

for R being Relation of the carrier of L holds

( R is multiplicative iff for a, x, y being Element of L st [a,x] in R & [a,y] in R holds

[a,(x "/\" y)] in R );

for L being non empty RelStr

for R being Relation of the carrier of L holds

( R is multiplicative iff for a, x, y being Element of L st [a,x] in R & [a,y] in R holds

[a,(x "/\" y)] in R );

registration

let L be lower-bounded sup-Semilattice;

let R be auxiliary Relation of L;

let x be Element of L;

coherence

R -above x is upper

end;
let R be auxiliary Relation of L;

let x be Element of L;

coherence

R -above x is upper

proof end;

:: Lemma 3.25: (1) iff (2)-[non empty]

theorem :: WAYBEL_7:40

for L being lower-bounded LATTICE

for R being auxiliary Relation of L holds

( R is multiplicative iff for x being Element of L holds R -above x is filtered )

for R being auxiliary Relation of L holds

( R is multiplicative iff for x being Element of L holds R -above x is filtered )

proof end;

:: Lemma 3.25: (1) iff (3)

theorem Th41: :: WAYBEL_7:41

for L being lower-bounded LATTICE

for R being auxiliary Relation of L holds

( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds

[(a "/\" b),(x "/\" y)] in R )

for R being auxiliary Relation of L holds

( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds

[(a "/\" b),(x "/\" y)] in R )

proof end;

:: Lemma 3.25: (1) iff (4)

theorem :: WAYBEL_7:42

for L being lower-bounded LATTICE

for R being auxiliary Relation of L holds

( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds

S is meet-inheriting )

for R being auxiliary Relation of L holds

( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds

S is meet-inheriting )

proof end;

:: Lemma 3.25: (1) iff (5)

theorem :: WAYBEL_7:43

for L being lower-bounded LATTICE

for R being auxiliary Relation of L holds

( R is multiplicative iff R -below is meet-preserving )

for R being auxiliary Relation of L holds

( R is multiplicative iff R -below is meet-preserving )

proof end;

Lm3: now :: thesis: for L being lower-bounded continuous LATTICE

for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) ) holds

p is prime

for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) ) holds

p is prime

let L be lower-bounded continuous LATTICE; :: thesis: for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) ) holds

p is prime

let p be Element of L; :: thesis: ( L -waybelow is multiplicative & ( for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) ) implies p is prime )

assume that

A1: L -waybelow is multiplicative and

A2: for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) and

A3: not p is prime ; :: thesis: contradiction

consider x, y being Element of L such that

A4: x "/\" y <= p and

A5: not x <= p and

A6: not y <= p by A3, WAYBEL_6:def 6;

A7: for a being Element of L holds

( not waybelow a is empty & waybelow a is directed ) ;

then consider u being Element of L such that

A8: u << x and

A9: not u <= p by A5, WAYBEL_3:24;

consider v being Element of L such that

A10: v << y and

A11: not v <= p by A6, A7, WAYBEL_3:24;

A12: [v,y] in L -waybelow by A10, WAYBEL_4:def 1;

[u,x] in L -waybelow by A8, WAYBEL_4:def 1;

then [(u "/\" v),(x "/\" y)] in L -waybelow by A1, A12, Th41;

then u "/\" v << x "/\" y by WAYBEL_4:def 1;

then u "/\" v << p by A4, WAYBEL_3:2;

hence contradiction by A2, A9, A11; :: thesis: verum

end;
( not a "/\" b << p or a <= p or b <= p ) ) holds

p is prime

let p be Element of L; :: thesis: ( L -waybelow is multiplicative & ( for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) ) implies p is prime )

assume that

A1: L -waybelow is multiplicative and

A2: for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) and

A3: not p is prime ; :: thesis: contradiction

consider x, y being Element of L such that

A4: x "/\" y <= p and

A5: not x <= p and

A6: not y <= p by A3, WAYBEL_6:def 6;

A7: for a being Element of L holds

( not waybelow a is empty & waybelow a is directed ) ;

then consider u being Element of L such that

A8: u << x and

A9: not u <= p by A5, WAYBEL_3:24;

consider v being Element of L such that

A10: v << y and

A11: not v <= p by A6, A7, WAYBEL_3:24;

A12: [v,y] in L -waybelow by A10, WAYBEL_4:def 1;

[u,x] in L -waybelow by A8, WAYBEL_4:def 1;

then [(u "/\" v),(x "/\" y)] in L -waybelow by A1, A12, Th41;

then u "/\" v << x "/\" y by WAYBEL_4:def 1;

then u "/\" v << p by A4, WAYBEL_3:2;

hence contradiction by A2, A9, A11; :: thesis: verum

theorem Th44: :: WAYBEL_7:44

for L being lower-bounded continuous LATTICE st L -waybelow is multiplicative holds

for p being Element of L holds

( p is pseudoprime iff for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) )

for p being Element of L holds

( p is pseudoprime iff for a, b being Element of L holds

( not a "/\" b << p or a <= p or b <= p ) )

proof end;

theorem :: WAYBEL_7:45

for L being lower-bounded continuous LATTICE st L -waybelow is multiplicative holds

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_7:46

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

p is prime ) holds

L -waybelow is multiplicative

p is prime ) holds

L -waybelow is multiplicative

proof end;