:: Set Sequences and Monotone Class
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for t, p, s being real number st 0 < s & t <= p holds
( t < p + s & t - s < p )
theorem Th1: :: PROB_3:1
theorem Th2: :: PROB_3:2
theorem Th3: :: PROB_3:3
theorem Th4: :: PROB_3:4
theorem Th5: :: PROB_3:5
theorem Th6: :: PROB_3:6
theorem Th7: :: PROB_3:7
theorem Th8: :: PROB_3:8
theorem Th9: :: PROB_3:9
:: deftheorem Def1 defines Partial_Intersection PROB_3:def 1 :
:: deftheorem Def2 defines Partial_Union PROB_3:def 2 :
theorem Th10: :: PROB_3:10
theorem Th11: :: PROB_3:11
theorem Th12: :: PROB_3:12
theorem Th13: :: PROB_3:13
theorem Th14: :: PROB_3:14
theorem Th15: :: PROB_3:15
theorem Th16: :: PROB_3:16
theorem Th17: :: PROB_3:17
theorem Th18: :: PROB_3:18
:: deftheorem Def3 defines Partial_Diff_Union PROB_3:def 3 :
theorem Th19: :: PROB_3:19
theorem Th20: :: PROB_3:20
theorem Th21: :: PROB_3:21
theorem Th22: :: PROB_3:22
theorem Th23: :: PROB_3:23
:: deftheorem Def4 defines disjoint_valued PROB_3:def 4 :
theorem Th24: :: PROB_3:24
:: deftheorem defines @Partial_Intersection PROB_3:def 5 :
:: deftheorem defines @Partial_Union PROB_3:def 6 :
:: deftheorem defines @Partial_Diff_Union PROB_3:def 7 :
theorem :: PROB_3:25
theorem :: PROB_3:26
theorem :: PROB_3:27
theorem :: PROB_3:28
theorem :: PROB_3:29
theorem :: PROB_3:30
theorem :: PROB_3:31
theorem :: PROB_3:32
theorem :: PROB_3:33
theorem :: PROB_3:34
theorem :: PROB_3:35
theorem :: PROB_3:36
theorem :: PROB_3:37
theorem :: PROB_3:38
theorem :: PROB_3:39
theorem :: PROB_3:40
theorem :: PROB_3:41
theorem Th42: :: PROB_3:42
theorem :: PROB_3:43
theorem :: PROB_3:44
theorem Th45: :: PROB_3:45
theorem Th46: :: PROB_3:46
theorem Th47: :: PROB_3:47
theorem Th48: :: PROB_3:48
theorem Th49: :: PROB_3:49
theorem Th50: :: PROB_3:50
theorem Th51: :: PROB_3:51
theorem Th52: :: PROB_3:52
theorem :: PROB_3:53
theorem Th54: :: PROB_3:54
:: deftheorem Def8 defines Complement PROB_3:def 8 :
:: deftheorem Def9 defines Intersection PROB_3:def 9 :
theorem Th55: :: PROB_3:55
theorem Th56: :: PROB_3:56
theorem Th57: :: PROB_3:57
theorem :: PROB_3:58
theorem Th59: :: PROB_3:59
theorem Th60: :: PROB_3:60
:: deftheorem Def10 defines FinSequence PROB_3:def 10 :
theorem Th61: :: PROB_3:61
theorem Th62: :: PROB_3:62
:: deftheorem defines @Complement PROB_3:def 11 :
theorem :: PROB_3:63
theorem Th64: :: PROB_3:64
theorem Th65: :: PROB_3:65
theorem Th66: :: PROB_3:66
theorem Th67: :: PROB_3:67
theorem Th68: :: PROB_3:68
theorem Th69: :: PROB_3:69
theorem :: PROB_3:70
:: deftheorem Def12 defines non-decreasing-closed PROB_3:def 12 :
:: deftheorem Def13 defines non-increasing-closed PROB_3:def 13 :
theorem Th71: :: PROB_3:71
theorem Th72: :: PROB_3:72
theorem Th73: :: PROB_3:73
theorem Th74: :: PROB_3:74
theorem Th75: :: PROB_3:75
theorem Th76: :: PROB_3:76
theorem Th77: :: PROB_3:77
:: deftheorem PROB_3:def 14 :
canceled;
:: deftheorem Def15 defines monotoneclass PROB_3:def 15 :
theorem Th78: :: PROB_3:78
theorem :: PROB_3:79