:: Sorting Operators for Finite Sequences
:: by Yatsuka Nakamura
::
:: Received October 17, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem Def1 defines max_p RFINSEQ2:def 1 :
:: deftheorem Def2 defines min_p RFINSEQ2:def 2 :
:: deftheorem defines max RFINSEQ2:def 3 :
:: deftheorem defines min RFINSEQ2:def 4 :
theorem Th1: :: RFINSEQ2:1
theorem Th2: :: RFINSEQ2:2
theorem :: RFINSEQ2:3
theorem :: RFINSEQ2:4
theorem :: RFINSEQ2:5
theorem :: RFINSEQ2:6
theorem :: RFINSEQ2:7
theorem :: RFINSEQ2:8
theorem :: RFINSEQ2:9
theorem :: RFINSEQ2:10
theorem :: RFINSEQ2:11
theorem :: RFINSEQ2:12
theorem :: RFINSEQ2:13
Lm1:
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
max f <= max g
theorem Th14: :: RFINSEQ2:14
Lm2:
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
min f >= min g
theorem Th15: :: RFINSEQ2:15
:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :
theorem Th16: :: RFINSEQ2:16
theorem Th17: :: RFINSEQ2:17
Lm3:
for f, g being non-decreasing FinSequence of REAL
for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
theorem Th18: :: RFINSEQ2:18
Lm4:
for n being Element of NAT
for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2
theorem Th19: :: RFINSEQ2:19
:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :
theorem :: RFINSEQ2:20
theorem :: RFINSEQ2:21
theorem :: RFINSEQ2:22
theorem :: RFINSEQ2:23
theorem Th24: :: RFINSEQ2:24
theorem Th25: :: RFINSEQ2:25
theorem Th26: :: RFINSEQ2:26
theorem Th27: :: RFINSEQ2:27
theorem :: RFINSEQ2:28
theorem :: RFINSEQ2:29
theorem Th30: :: RFINSEQ2:30
theorem Th31: :: RFINSEQ2:31
theorem :: RFINSEQ2:32