:: On Rectangular Finite Sequences of the Points of the Plane
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received November 30, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem :: SPRECT_1:1
canceled;
theorem :: SPRECT_1:2
canceled;
theorem Th3: :: SPRECT_1:3
theorem Th4: :: SPRECT_1:4
theorem Th5: :: SPRECT_1:5
theorem Th6: :: SPRECT_1:6
theorem Th7: :: SPRECT_1:7
theorem Th8: :: SPRECT_1:8
theorem Th9: :: SPRECT_1:9
theorem Th10: :: SPRECT_1:10
theorem Th11: :: SPRECT_1:11
theorem Th12: :: SPRECT_1:12
theorem Th13: :: SPRECT_1:13
theorem Th14: :: SPRECT_1:14
theorem Th15: :: SPRECT_1:15
theorem Th16: :: SPRECT_1:16
theorem Th17: :: SPRECT_1:17
theorem Th18: :: SPRECT_1:18
theorem :: SPRECT_1:19
theorem :: SPRECT_1:20
theorem :: SPRECT_1:21
theorem :: SPRECT_1:22
theorem Th23: :: SPRECT_1:23
theorem Th24: :: SPRECT_1:24
theorem Th25: :: SPRECT_1:25
theorem Th26: :: SPRECT_1:26
theorem Th27: :: SPRECT_1:27
theorem Th28: :: SPRECT_1:28
theorem :: SPRECT_1:29
theorem Th30: :: SPRECT_1:30
theorem Th31: :: SPRECT_1:31
theorem Th32: :: SPRECT_1:32
theorem Th33: :: SPRECT_1:33
theorem Th34: :: SPRECT_1:34
theorem Th35: :: SPRECT_1:35
theorem Th36: :: SPRECT_1:36
:: deftheorem defines SpStSeq SPRECT_1:def 1 :
theorem Th37: :: SPRECT_1:37
theorem Th38: :: SPRECT_1:38
theorem Th39: :: SPRECT_1:39
theorem Th40: :: SPRECT_1:40
theorem :: SPRECT_1:41
theorem Th42: :: SPRECT_1:42
theorem Th43: :: SPRECT_1:43
theorem Th44: :: SPRECT_1:44
theorem :: SPRECT_1:45
canceled;
theorem Th46: :: SPRECT_1:46
theorem Th47: :: SPRECT_1:47
theorem Th48: :: SPRECT_1:48
theorem Th49: :: SPRECT_1:49
theorem Th50: :: SPRECT_1:50
theorem Th51: :: SPRECT_1:51
theorem Th52: :: SPRECT_1:52
theorem Th53: :: SPRECT_1:53
theorem Th54: :: SPRECT_1:54
theorem Th55: :: SPRECT_1:55
theorem Th56: :: SPRECT_1:56
theorem Th57: :: SPRECT_1:57
theorem :: SPRECT_1:58
canceled;
theorem Th59: :: SPRECT_1:59
for
r1,
r2,
t being
Real st
r1 <= r2 holds
(
t in [.r1,r2.] iff ex
s1 being
Real st
(
0 <= s1 &
s1 <= 1 &
t = (s1 * r1) + ((1 - s1) * r2) ) )
theorem Th60: :: SPRECT_1:60
theorem Th61: :: SPRECT_1:61
theorem Th62: :: SPRECT_1:62
theorem Th63: :: SPRECT_1:63
theorem Th64: :: SPRECT_1:64
theorem Th65: :: SPRECT_1:65
theorem Th66: :: SPRECT_1:66
theorem Th67: :: SPRECT_1:67
theorem Th68: :: SPRECT_1:68
theorem Th69: :: SPRECT_1:69
theorem Th70: :: SPRECT_1:70
theorem Th71: :: SPRECT_1:71
theorem Th72: :: SPRECT_1:72
theorem Th73: :: SPRECT_1:73
theorem Th74: :: SPRECT_1:74
theorem Th75: :: SPRECT_1:75
theorem Th76: :: SPRECT_1:76
theorem Th77: :: SPRECT_1:77
theorem Th78: :: SPRECT_1:78
theorem Th79: :: SPRECT_1:79
theorem Th80: :: SPRECT_1:80
theorem Th81: :: SPRECT_1:81
theorem Th82: :: SPRECT_1:82
theorem Th83: :: SPRECT_1:83
theorem Th84: :: SPRECT_1:84
theorem Th85: :: SPRECT_1:85
theorem Th86: :: SPRECT_1:86
theorem Th87: :: SPRECT_1:87
theorem Th88: :: SPRECT_1:88
theorem Th89: :: SPRECT_1:89
:: deftheorem Def2 defines rectangular SPRECT_1:def 2 :
theorem :: SPRECT_1:90
theorem :: SPRECT_1:91
theorem :: SPRECT_1:92
theorem :: SPRECT_1:93
theorem :: SPRECT_1:94
theorem Th95: :: SPRECT_1:95
for
r1,
r2,
s1,
s2 being
Real st
r1 < r2 &
s1 < s2 holds
[.r1,r2,s1,s2.] is
Jordan
:: deftheorem Def3 defines Jordan SPRECT_1:def 3 :
theorem Th96: :: SPRECT_1:96
theorem :: SPRECT_1:97