:: Irreducible and Prime Elements
:: by Beata Madras
::
:: Received December 1, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem Th1: :: WAYBEL_6:1
theorem Th2: :: WAYBEL_6:2
theorem Th3: :: WAYBEL_6:3
Lm1:
for S, T being non empty with_suprema Poset
for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
theorem Th4: :: WAYBEL_6:4
:: deftheorem Def1 defines Open WAYBEL_6:def 1 :
theorem :: WAYBEL_6:5
theorem :: WAYBEL_6:6
theorem :: WAYBEL_6:7
theorem Th8: :: WAYBEL_6:8
theorem Th9: :: WAYBEL_6:9
:: deftheorem Def2 defines meet-irreducible WAYBEL_6:def 2 :
:: deftheorem defines join-irreducible WAYBEL_6:def 3 :
:: deftheorem Def4 defines IRR WAYBEL_6:def 4 :
theorem Th10: :: WAYBEL_6:10
theorem :: WAYBEL_6:11
theorem :: WAYBEL_6:12
theorem Th13: :: WAYBEL_6:13
theorem Th14: :: WAYBEL_6:14
:: deftheorem Def5 defines order-generating WAYBEL_6:def 5 :
theorem Th15: :: WAYBEL_6:15
theorem :: WAYBEL_6:16
theorem Th17: :: WAYBEL_6:17
theorem Th18: :: WAYBEL_6:18
theorem Th19: :: WAYBEL_6:19
:: deftheorem Def6 defines prime WAYBEL_6:def 6 :
:: deftheorem Def7 defines PRIME WAYBEL_6:def 7 :
:: deftheorem Def8 defines co-prime WAYBEL_6:def 8 :
theorem Th20: :: WAYBEL_6:20
theorem :: WAYBEL_6:21
theorem Th22: :: WAYBEL_6:22
theorem Th23: :: WAYBEL_6:23
theorem Th24: :: WAYBEL_6:24
theorem Th25: :: WAYBEL_6:25
theorem Th26: :: WAYBEL_6:26
theorem Th27: :: WAYBEL_6:27
theorem Th28: :: WAYBEL_6:28
theorem :: WAYBEL_6:29
theorem :: WAYBEL_6:30
theorem Th31: :: WAYBEL_6:31
theorem Th32: :: WAYBEL_6:32
theorem Th33: :: WAYBEL_6:33
theorem Th34: :: WAYBEL_6:34
theorem Th35: :: WAYBEL_6:35
theorem :: WAYBEL_6:36
theorem Th37: :: WAYBEL_6:37
Lm2:
for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) holds
L is completely-distributive
Lm3:
for L being complete completely-distributive LATTICE holds
( L is distributive & L is continuous & L ~ is continuous )
Lm4:
for L being complete LATTICE st L is distributive & L is continuous & L ~ is continuous holds
for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) )
theorem :: WAYBEL_6:38
theorem :: WAYBEL_6:39