:: Basic Properties and Concept of Selected Subsequence of Zero Based FiniteSequences
:: by Yatsuka Nakamura and Hisashi Ito
::
:: Received June 27, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem AB470: :: AFINSQ_2:1
theorem AE221f: :: AFINSQ_2:2
theorem Th11: :: AFINSQ_2:3
theorem Th14: :: AFINSQ_2:4
theorem Th10: :: AFINSQ_2:5
theorem AC500: :: AFINSQ_2:6
theorem AE359: :: AFINSQ_2:7
:: deftheorem Def3 defines Rev AFINSQ_2:def 1 :
theorem Th60: :: AFINSQ_2:8
theorem :: AFINSQ_2:9
theorem Lm4: :: AFINSQ_2:10
theorem Th19: :: AFINSQ_2:11
theorem TH80: :: AFINSQ_2:12
theorem TH80f: :: AFINSQ_2:13
theorem :: AFINSQ_2:14
:: deftheorem Def2 defines /^ AFINSQ_2:def 2 :
theorem TH80e: :: AFINSQ_2:15
theorem TH80b: :: AFINSQ_2:16
theorem Th19b: :: AFINSQ_2:17
theorem AG170: :: AFINSQ_2:18
theorem Th31: :: AFINSQ_2:19
theorem Th39: :: AFINSQ_2:20
theorem Th40: :: AFINSQ_2:21
theorem :: AFINSQ_2:22
:: deftheorem AB540b defines mid AFINSQ_2:def 3 :
theorem AB540f: :: AFINSQ_2:23
theorem :: AFINSQ_2:24
theorem Th5: :: AFINSQ_2:25
theorem :: AFINSQ_2:26
theorem :: AFINSQ_2:27
theorem :: AFINSQ_2:28
:: deftheorem AC300 defines Sum AFINSQ_2:def 4 :
theorem :: AFINSQ_2:29
theorem :: AFINSQ_2:30
definition
let X be
finite natural-membered set ;
func Sgm0 X -> XFinSequence of
NAT means :
AC113:
:: AFINSQ_2:def 5
(
rng it = X & ( for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len it &
k1 = it . l &
k2 = it . m holds
k1 < k2 ) );
existence
ex b1 being XFinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
uniqueness
for b1, b2 being XFinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
end;
:: deftheorem AC113 defines Sgm0 AFINSQ_2:def 5 :
theorem Th44: :: AFINSQ_2:31
theorem AE200: :: AFINSQ_2:32
theorem AE205: :: AFINSQ_2:33
:: deftheorem AE100 defines <N< AFINSQ_2:def 6 :
for
B1,
B2 being
set holds
(
B1 <N< B2 iff for
n,
m being
Nat st
n in B1 &
m in B2 holds
n < m );
:: deftheorem AE102 defines <N= AFINSQ_2:def 7 :
for
B1,
B2 being
set holds
(
B1 <N= B2 iff for
n,
m being
Nat st
n in B1 &
m in B2 holds
n <= m );
theorem AG110: :: AFINSQ_2:34
theorem AE101: :: AFINSQ_2:35
theorem AE400: :: AFINSQ_2:36
theorem :: AFINSQ_2:37
theorem AE221e: :: AFINSQ_2:38
theorem :: AFINSQ_2:39
theorem AE221: :: AFINSQ_2:40
theorem AE222e: :: AFINSQ_2:41
theorem AE222f: :: AFINSQ_2:42
theorem AE222: :: AFINSQ_2:43
theorem Th46: :: AFINSQ_2:44
theorem AE220: :: AFINSQ_2:45
theorem :: AFINSQ_2:46
:: deftheorem defines SubXFinS AFINSQ_2:def 8 :
theorem AC200: :: AFINSQ_2:47
theorem :: AFINSQ_2:48