:: On the Closure Operator and the Closure System of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received February 7, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: CLOSURE2:1
theorem :: CLOSURE2:2
canceled;
theorem Th3: :: CLOSURE2:3
:: deftheorem Def1 defines Bool CLOSURE2:def 1 :
theorem Th4: :: CLOSURE2:4
theorem :: CLOSURE2:5
theorem :: CLOSURE2:6
theorem :: CLOSURE2:7
theorem Th8: :: CLOSURE2:8
theorem Th9: :: CLOSURE2:9
theorem Th10: :: CLOSURE2:10
theorem Th11: :: CLOSURE2:11
theorem :: CLOSURE2:12
theorem :: CLOSURE2:13
:: deftheorem CLOSURE2:def 2 :
canceled;
:: deftheorem Def3 defines |. CLOSURE2:def 3 :
theorem Th14: :: CLOSURE2:14
:: deftheorem Def4 defines |: CLOSURE2:def 4 :
theorem Th15: :: CLOSURE2:15
theorem Th16: :: CLOSURE2:16
theorem :: CLOSURE2:17
theorem Th18: :: CLOSURE2:18
theorem :: CLOSURE2:19
theorem Th20: :: CLOSURE2:20
theorem Th21: :: CLOSURE2:21
theorem Th22: :: CLOSURE2:22
theorem Th23: :: CLOSURE2:23
theorem Th24: :: CLOSURE2:24
theorem Th25: :: CLOSURE2:25
theorem :: CLOSURE2:26
:: deftheorem defines additive CLOSURE2:def 5 :
:: deftheorem Def6 defines absolutely-additive CLOSURE2:def 6 :
:: deftheorem defines multiplicative CLOSURE2:def 7 :
:: deftheorem Def8 defines absolutely-multiplicative CLOSURE2:def 8 :
:: deftheorem Def9 defines properly-upper-bound CLOSURE2:def 9 :
:: deftheorem Def10 defines properly-lower-bound CLOSURE2:def 10 :
Lm1:
for I being set
for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
:: deftheorem CLOSURE2:def 11 :
canceled;
:: deftheorem Def12 defines reflexive CLOSURE2:def 12 :
:: deftheorem Def13 defines monotonic CLOSURE2:def 13 :
:: deftheorem Def14 defines idempotent CLOSURE2:def 14 :
:: deftheorem Def15 defines topological CLOSURE2:def 15 :
theorem :: CLOSURE2:27
theorem :: CLOSURE2:28
theorem :: CLOSURE2:29
theorem :: CLOSURE2:30
theorem :: CLOSURE2:31
theorem :: CLOSURE2:32
theorem :: CLOSURE2:33
theorem :: CLOSURE2:34
theorem :: CLOSURE2:35
theorem :: CLOSURE2:36
theorem :: CLOSURE2:37
theorem :: CLOSURE2:38
:: deftheorem Def16 defines additive CLOSURE2:def 16 :
:: deftheorem Def17 defines absolutely-additive CLOSURE2:def 17 :
:: deftheorem Def18 defines multiplicative CLOSURE2:def 18 :
:: deftheorem Def19 defines absolutely-multiplicative CLOSURE2:def 19 :
:: deftheorem Def20 defines properly-upper-bound CLOSURE2:def 20 :
:: deftheorem Def21 defines properly-lower-bound CLOSURE2:def 21 :
:: deftheorem defines Full CLOSURE2:def 22 :
theorem Th39: :: CLOSURE2:39
:: deftheorem Def23 defines ClOp->ClSys CLOSURE2:def 23 :
:: deftheorem Def24 defines Cl CLOSURE2:def 24 :
theorem Th40: :: CLOSURE2:40
theorem :: CLOSURE2:41
theorem Th42: :: CLOSURE2:42
:: deftheorem Def25 defines ClSys->ClOp CLOSURE2:def 25 :
theorem :: CLOSURE2:43
deffunc H1( set ) -> set = $1;
theorem :: CLOSURE2:44