:: LATTICE6 semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
Lm1:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
Lm2:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
Lm3:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
Lm4:
for L being finite Lattice ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a
Lm5:
for L being finite Lattice holds L is complete
:: deftheorem defines % LATTICE6:def 1 :
:: deftheorem defines % LATTICE6:def 2 :
Lm6:
for L being finite Lattice holds (LattPOSet L) ~ is well_founded
:: deftheorem Def3 defines noetherian LATTICE6:def 3 :
:: deftheorem Def4 defines co-noetherian LATTICE6:def 4 :
theorem :: LATTICE6:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm7:
for L being finite Lattice holds
( L is noetherian & L is co-noetherian )
:: deftheorem Def5 defines is-upper-neighbour-of LATTICE6:def 5 :
theorem Th2: :: LATTICE6:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th3: :: LATTICE6:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th4: :: LATTICE6:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th5: :: LATTICE6:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th6: :: LATTICE6:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: LATTICE6:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th8: :: LATTICE6:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines *' LATTICE6:def 6 :
:: deftheorem defines *' LATTICE6:def 7 :
:: deftheorem Def8 defines completely-meet-irreducible LATTICE6:def 8 :
:: deftheorem Def9 defines completely-join-irreducible LATTICE6:def 9 :
theorem Th9: :: LATTICE6:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: LATTICE6:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: LATTICE6:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th12: :: LATTICE6:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th13: :: LATTICE6:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th14: :: LATTICE6:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th15: :: LATTICE6:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th16: :: LATTICE6:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm8:
for L being Lattice
for a, b being Element of L holds
( a "/\" b = (a % ) "/\" (b % ) & a "\/" b = (a % ) "\/" (b % ) )
theorem Th17: :: LATTICE6:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th18: :: LATTICE6:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th19: :: LATTICE6:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: LATTICE6:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def10 defines atomic LATTICE6:def 10 :
:: deftheorem Def11 defines co-atomic LATTICE6:def 11 :
theorem :: LATTICE6:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: LATTICE6:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def12 defines atomic LATTICE6:def 12 :
Lm9:
ex L being Lattice st
( L is atomic & L is complete )
:: deftheorem Def13 defines supremum-dense LATTICE6:def 13 :
:: deftheorem Def14 defines infimum-dense LATTICE6:def 14 :
theorem Th23: :: LATTICE6:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th24: :: LATTICE6:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: LATTICE6:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines MIRRS LATTICE6:def 15 :
:: deftheorem defines JIRRS LATTICE6:def 16 :
theorem :: LATTICE6:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: LATTICE6:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm10:
for L being complete co-noetherian Lattice holds MIRRS L is infimum-dense
Lm11:
for L being complete noetherian Lattice holds JIRRS L is supremum-dense