:: More on the Finite Sequences on the Plane
:: by Andrzej Trybulec
::
:: Received October 25, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem Th1: :: TOPREAL8:1
for
A,
x,
y being
set st
A c= {x,y} &
x in A & not
y in A holds
A = {x}
theorem Th2: :: TOPREAL8:2
theorem Th3: :: TOPREAL8:3
theorem Th4: :: TOPREAL8:4
theorem Th5: :: TOPREAL8:5
theorem Th6: :: TOPREAL8:6
theorem Th7: :: TOPREAL8:7
theorem Th8: :: TOPREAL8:8
theorem :: TOPREAL8:9
theorem Th10: :: TOPREAL8:10
theorem Th11: :: TOPREAL8:11
theorem Th12: :: TOPREAL8:12
Lm1:
for p being FinSequence
for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds
( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) )
theorem Th13: :: TOPREAL8:13
theorem Th14: :: TOPREAL8:14
theorem Th15: :: TOPREAL8:15
theorem Th16: :: TOPREAL8:16
theorem Th17: :: TOPREAL8:17
theorem Th18: :: TOPREAL8:18
theorem Th19: :: TOPREAL8:19
theorem Th20: :: TOPREAL8:20
theorem Th21: :: TOPREAL8:21
theorem Th22: :: TOPREAL8:22
theorem Th23: :: TOPREAL8:23
theorem Th24: :: TOPREAL8:24
theorem Th25: :: TOPREAL8:25
theorem Th26: :: TOPREAL8:26
theorem Th27: :: TOPREAL8:27
theorem Th28: :: TOPREAL8:28
theorem Th29: :: TOPREAL8:29
theorem Th30: :: TOPREAL8:30
theorem Th31: :: TOPREAL8:31
theorem Th32: :: TOPREAL8:32
Lm2:
for f being one-to-one non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st i < len f & 1 < i holds
for x being Point of (TOP-REAL 2) st x in (LSeg (f ^' g),i) /\ (LSeg (f ^' g),j) holds
x <> f /. 1
Lm3:
for f being one-to-one non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st j > len f & j + 1 < len (f ^' g) holds
for x being Point of (TOP-REAL 2) st x in (LSeg (f ^' g),i) /\ (LSeg (f ^' g),j) holds
x <> g /. (len g)
theorem Th33: :: TOPREAL8:33
theorem Th34: :: TOPREAL8:34
theorem Th35: :: TOPREAL8:35
theorem :: TOPREAL8:36