:: Meet Continuous Lattices Revisited
:: by Artur Korni{\l}owicz
::
:: Received January 6, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: WAYBEL30:1
theorem Th2: :: WAYBEL30:2
theorem Th3: :: WAYBEL30:3
theorem Th4: :: WAYBEL30:4
theorem :: WAYBEL30:5
theorem :: WAYBEL30:6
theorem :: WAYBEL30:7
theorem Th8: :: WAYBEL30:8
theorem Th9: :: WAYBEL30:9
theorem Th10: :: WAYBEL30:10
theorem :: WAYBEL30:11
theorem Th12: :: WAYBEL30:12
theorem Th13: :: WAYBEL30:13
theorem Th14: :: WAYBEL30:14
theorem Th15: :: WAYBEL30:15
theorem Th16: :: WAYBEL30:16
theorem Th17: :: WAYBEL30:17
theorem :: WAYBEL30:18
theorem Th19: :: WAYBEL30:19
theorem Th20: :: WAYBEL30:20
theorem Th21: :: WAYBEL30:21
theorem Th22: :: WAYBEL30:22
Lm3:
now
let S,
T,
x1,
x2 be
set ;
:: thesis: ( x1 in S & x2 in T implies <:(pr2 S,T),(pr1 S,T):> . [x1,x2] = [x2,x1] )assume that A1:
x1 in S
and A2:
x2 in T
;
:: thesis: <:(pr2 S,T),(pr1 S,T):> . [x1,x2] = [x2,x1]A3:
dom <:(pr2 S,T),(pr1 S,T):> =
(dom (pr2 S,T)) /\ (dom (pr1 S,T))
by FUNCT_3:def 8
.=
(dom (pr2 S,T)) /\ [:S,T:]
by FUNCT_3:def 5
.=
[:S,T:] /\ [:S,T:]
by FUNCT_3:def 6
.=
[:S,T:]
;
[x1,x2] in [:S,T:]
by A1, A2, ZFMISC_1:106;
hence <:(pr2 S,T),(pr1 S,T):> . [x1,x2] =
[((pr2 S,T) . x1,x2),((pr1 S,T) . x1,x2)]
by A3, FUNCT_3:def 8
.=
[x2,((pr1 S,T) . x1,x2)]
by A1, A2, FUNCT_3:def 6
.=
[x2,x1]
by A1, A2, FUNCT_3:def 5
;
:: thesis: verum
end;
theorem :: WAYBEL30:23
:: deftheorem defines ^0 WAYBEL30:def 1 :
theorem :: WAYBEL30:24
theorem Th25: :: WAYBEL30:25
theorem Th26: :: WAYBEL30:26
theorem Th27: :: WAYBEL30:27
theorem Th28: :: WAYBEL30:28
theorem Th29: :: WAYBEL30:29
theorem Th30: :: WAYBEL30:30
:: deftheorem defines with_small_semilattices WAYBEL30:def 2 :
:: deftheorem defines with_compact_semilattices WAYBEL30:def 3 :
:: deftheorem Def4 defines with_open_semilattices WAYBEL30:def 4 :
theorem Th31: :: WAYBEL30:31
theorem Th32: :: WAYBEL30:32
theorem Th33: :: WAYBEL30:33
theorem Th34: :: WAYBEL30:34
theorem Th35: :: WAYBEL30:35
theorem :: WAYBEL30:36
theorem :: WAYBEL30:37
theorem :: WAYBEL30:38
theorem :: WAYBEL30:39
theorem Th40: :: WAYBEL30:40