:: WAYBEL13 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: WAYBEL13:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive RelStr
for x, y being Element of L st x <= y holds
compactbelow x c= compactbelow y
proof end;

theorem Th2: :: WAYBEL13:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x is Subset of (CompactSublatt L)
proof end;

theorem Th3: :: WAYBEL13:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for S being SubRelStr of L
for X being Subset of S holds X is Subset of L
proof end;

theorem Th4: :: WAYBEL13:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive transitive with_suprema RelStr holds the carrier of L is Ideal of L
proof end;

theorem Th5: :: WAYBEL13:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1 being non empty reflexive antisymmetric lower-bounded RelStr
for 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
the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)
proof end;

theorem Th6: :: WAYBEL13:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded algebraic LATTICE
for S being CLSubFrame of L holds S is algebraic
proof end;

theorem Th7: :: WAYBEL13:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, E being set
for L being CLSubFrame of BoolePoset X holds
( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )
proof end;

theorem Th8: :: WAYBEL13:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L
proof end;

registration
let L be non empty reflexive transitive RelStr ;
cluster principal Element of bool the carrier of L;
existence
ex b1 being Ideal of L st b1 is principal
proof end;
end;

theorem Th9: :: WAYBEL13:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded sup-Semilattice
for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X
proof end;

theorem Th10: :: WAYBEL13:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being lower-bounded sup-Semilattice holds InclPoset (Ids S) is algebraic
proof end;

theorem Th11: :: WAYBEL13:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being lower-bounded sup-Semilattice
for x being Element of (InclPoset (Ids S)) holds
( x is compact iff x is principal Ideal of S )
proof end;

theorem Th12: :: WAYBEL13:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being lower-bounded sup-Semilattice
for x being Element of (InclPoset (Ids S)) holds
( x is compact iff ex a being Element of S st x = downarrow a )
proof end;

theorem :: WAYBEL13:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded sup-Semilattice
for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds
f is isomorphic
proof end;

theorem :: WAYBEL13:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being lower-bounded LATTICE holds InclPoset (Ids S) is arithmetic
proof end;

theorem Th15: :: WAYBEL13:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded sup-Semilattice holds CompactSublatt L is lower-bounded sup-Semilattice
proof end;

theorem Th16: :: WAYBEL13:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded algebraic sup-Semilattice
for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds
f is isomorphic
proof end;

theorem :: WAYBEL13:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded algebraic sup-Semilattice
for x being Element of L holds
( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )
proof end;

theorem Th18: :: WAYBEL13:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty RelStr
for X being Subset of L1
for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_<=_than X iff f . x is_<=_than f .: X )
proof end;

theorem Th19: :: WAYBEL13:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty RelStr
for X being Subset of L1
for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_>=_than X iff f . x is_>=_than f .: X )
proof end;

theorem Th20: :: WAYBEL13:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty antisymmetric RelStr
for f being Function of L1,L2 st f is isomorphic holds
( f is infs-preserving & f is sups-preserving )
proof end;

registration
let L1, L2 be non empty antisymmetric RelStr ;
cluster isomorphic -> infs-preserving sups-preserving M4(the carrier of L1,the carrier of L2);
coherence
for b1 being Function of L1,L2 st b1 is isomorphic holds
( b1 is infs-preserving & b1 is sups-preserving )
by Th20;
end;

theorem Th21: :: WAYBEL13:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, L3 being non empty transitive antisymmetric RelStr
for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds
ex g being Function of L1,L3 st
( f = g & g is infs-preserving )
proof end;

theorem Th22: :: WAYBEL13:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, L3 being non empty transitive antisymmetric RelStr
for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds
ex g being Function of L1,L3 st
( f = g & g is directed-sups-preserving )
proof end;

theorem Th23: :: WAYBEL13:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded sup-Semilattice holds InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L)
proof end;

Lm1: for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is sups-preserving holds
f is directed-sups-preserving
proof end;

theorem Th24: :: WAYBEL13:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded algebraic LATTICE ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g is infs-preserving & g is directed-sups-preserving & g is one-to-one & ( for x being Element of L holds g . x = compactbelow x ) )
proof end;

theorem :: WAYBEL13:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) holds
product J is lower-bounded algebraic LATTICE
proof end;

Lm2: for L being lower-bounded LATTICE st L is algebraic holds
ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
proof end;

theorem Th26: :: WAYBEL13:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
L1,L2 are_isomorphic
proof end;

Lm3: for L being LATTICE st ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds
ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
proof end;

Lm4: for L being LATTICE st ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds
ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
proof end;

Lm5: for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 st x << y holds
f . x << f . y
proof end;

theorem Th27: :: WAYBEL13:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 holds
( x << y iff f . x << f . y )
proof end;

theorem Th28: :: WAYBEL13:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds
( x is compact iff f . x is compact )
proof end;

theorem Th29: :: WAYBEL13:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x)
proof end;

theorem Th30: :: WAYBEL13:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is up-complete holds
L2 is up-complete
proof end;

theorem Th31: :: WAYBEL13:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is complete & L1 is satisfying_axiom_K holds
L2 is satisfying_axiom_K
proof end;

theorem Th32: :: WAYBEL13:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being sup-Semilattice st L1,L2 are_isomorphic & L1 is lower-bounded & L1 is algebraic holds
L2 is algebraic
proof end;

Lm6: for L being LATTICE st ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) holds
L is algebraic
proof end;

theorem :: WAYBEL13:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded continuous sup-Semilattice holds
( SupMap L is infs-preserving & SupMap L is sups-preserving )
proof end;

theorem :: WAYBEL13:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded LATTICE holds
( ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) & ( ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) )
proof end;

theorem :: WAYBEL13:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded LATTICE holds
( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) )
proof end;