:: Some Properties of Dyadic Numbers and Intervals
:: by J\'ozef Bia{\l}as and Yatsuka Nakamura
::
:: Received February 16, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem :: URYSOHN2:1
canceled;
theorem Th2: :: URYSOHN2:2
theorem Th3: :: URYSOHN2:3
theorem Th4: :: URYSOHN2:4
theorem Th5: :: URYSOHN2:5
theorem Th6: :: URYSOHN2:6
theorem :: URYSOHN2:7
canceled;
theorem Th8: :: URYSOHN2:8
theorem Th9: :: URYSOHN2:9
theorem Th10: :: URYSOHN2:10
theorem Th11: :: URYSOHN2:11
theorem Th12: :: URYSOHN2:12
theorem Th13: :: URYSOHN2:13
theorem Th14: :: URYSOHN2:14
theorem :: URYSOHN2:15
theorem :: URYSOHN2:16
theorem :: URYSOHN2:17
theorem :: URYSOHN2:18
theorem Th19: :: URYSOHN2:19
Lx1:
for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_above holds
A is bounded_above
theorem Tx1: :: URYSOHN2:20
Lx2:
for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_below holds
A is bounded_below
theorem Tx2: :: URYSOHN2:21
theorem :: URYSOHN2:22
theorem Th23: :: URYSOHN2:23
theorem Th24: :: URYSOHN2:24
theorem :: URYSOHN2:25
canceled;
theorem :: URYSOHN2:26
canceled;
theorem :: URYSOHN2:27
theorem Th28: :: URYSOHN2:28
theorem Th29: :: URYSOHN2:29
for
a,
b being
Real st
a < b holds
ex
c being
Real st
(
c in DOM &
a < c &
c < b )
theorem :: URYSOHN2:30
theorem :: URYSOHN2:31
theorem :: URYSOHN2:32
theorem :: URYSOHN2:33
theorem Th34: :: URYSOHN2:34
for
a,
b,
c,
d being
Real st
a < c &
c < b &
a < d &
d < b holds
abs (d - c) < b - a
theorem :: URYSOHN2:35
theorem :: URYSOHN2:36
theorem :: URYSOHN2:37