:: Submetric Spaces - Part I
:: by Adam Lecko and Mariusz Startek
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: SUB_METR:1
theorem Th2: :: SUB_METR:2
theorem :: SUB_METR:3
canceled;
theorem Th4: :: SUB_METR:4
theorem Th5: :: SUB_METR:5
theorem Th6: :: SUB_METR:6
theorem Th7: :: SUB_METR:7
theorem Th8: :: SUB_METR:8
set M0 = MetrStruct(# 1,Empty^2-to-zero #);
:: deftheorem Def1 defines Discerning SUB_METR:def 1 :
:: deftheorem Def2 defines Discerning SUB_METR:def 2 :
theorem :: SUB_METR:9
canceled;
theorem :: SUB_METR:10
canceled;
theorem :: SUB_METR:11
canceled;
theorem :: SUB_METR:12
canceled;
theorem :: SUB_METR:13
canceled;
theorem Th14: :: SUB_METR:14
theorem :: SUB_METR:15
canceled;
theorem :: SUB_METR:16
canceled;
theorem :: SUB_METR:17
canceled;
theorem Th18: :: SUB_METR:18
:: deftheorem SUB_METR:def 3 :
canceled;
:: deftheorem Def4 defines ultra SUB_METR:def 4 :
definition
func Set_to_zero -> Function of
[:{{} ,{{} }},{{} ,{{} }}:],
REAL equals :: SUB_METR:def 5
[:{{} ,{{} }},{{} ,{{} }}:] --> 0 ;
coherence
[:{{} ,{{} }},{{} ,{{} }}:] --> 0 is Function of [:{{} ,{{} }},{{} ,{{} }}:], REAL
;
end;
:: deftheorem defines Set_to_zero SUB_METR:def 5 :
theorem :: SUB_METR:19
canceled;
theorem :: SUB_METR:20
canceled;
theorem :: SUB_METR:21
canceled;
theorem :: SUB_METR:22
canceled;
theorem :: SUB_METR:23
canceled;
theorem :: SUB_METR:24
canceled;
theorem :: SUB_METR:25
canceled;
theorem :: SUB_METR:26
canceled;
theorem :: SUB_METR:27
canceled;
theorem :: SUB_METR:28
canceled;
theorem :: SUB_METR:29
canceled;
theorem :: SUB_METR:30
canceled;
theorem :: SUB_METR:31
canceled;
theorem :: SUB_METR:32
canceled;
theorem :: SUB_METR:33
canceled;
theorem :: SUB_METR:34
canceled;
theorem :: SUB_METR:35
canceled;
theorem :: SUB_METR:36
canceled;
theorem :: SUB_METR:37
canceled;
theorem :: SUB_METR:38
canceled;
theorem :: SUB_METR:39
canceled;
theorem Th40: :: SUB_METR:40
theorem :: SUB_METR:41
canceled;
theorem Th42: :: SUB_METR:42
theorem Th43: :: SUB_METR:43
:: deftheorem defines ZeroSpace SUB_METR:def 6 :
:: deftheorem Def7 defines is_between SUB_METR:def 7 :
theorem :: SUB_METR:44
canceled;
theorem :: SUB_METR:45
canceled;
theorem :: SUB_METR:46
canceled;
theorem :: SUB_METR:47
theorem :: SUB_METR:48
theorem :: SUB_METR:49
:: deftheorem defines open_dist_Segment SUB_METR:def 8 :
theorem :: SUB_METR:50
canceled;
theorem :: SUB_METR:51
:: deftheorem defines close_dist_Segment SUB_METR:def 9 :
theorem :: SUB_METR:52
canceled;
theorem :: SUB_METR:53