:: Intermediate Value Theorem and Thickness of Simple Closed Curves
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received November 13, 1997
:: Copyright (c) 1997 Association of Mizar Users
Lm1:
for X, Y, Z being non empty TopSpace
for f being continuous Function of X,Y
for g being continuous Function of Y,Z holds g * f is continuous Function of X,Z
;
theorem :: TOPREAL5:1
canceled;
theorem :: TOPREAL5:2
canceled;
theorem :: TOPREAL5:3
canceled;
theorem Th4: :: TOPREAL5:4
theorem :: TOPREAL5:5
canceled;
theorem Th6: :: TOPREAL5:6
theorem :: TOPREAL5:7
canceled;
theorem :: TOPREAL5:8
canceled;
theorem Th9: :: TOPREAL5:9
theorem :: TOPREAL5:10
theorem :: TOPREAL5:11
theorem Th12: :: TOPREAL5:12
theorem Th13: :: TOPREAL5:13
theorem :: TOPREAL5:14
theorem Th15: :: TOPREAL5:15
theorem Th16: :: TOPREAL5:16
theorem Th17: :: TOPREAL5:17
theorem Th18: :: TOPREAL5:18
theorem Th19: :: TOPREAL5:19
theorem Th20: :: TOPREAL5:20
theorem Th21: :: TOPREAL5:21
theorem Th22: :: TOPREAL5:22
theorem Th23: :: TOPREAL5:23
theorem :: TOPREAL5:24
theorem :: TOPREAL5:25