:: On the Minimal Distance Between Set in {E}uclidean Space
:: by Andrzej Trybulec
::
:: Received August 19, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: JORDAN1K:1
theorem :: JORDAN1K:2
theorem Th3: :: JORDAN1K:3
theorem Th4: :: JORDAN1K:4
theorem Th5: :: JORDAN1K:5
theorem Th6: :: JORDAN1K:6
theorem Th7: :: JORDAN1K:7
theorem :: JORDAN1K:8
theorem Th9: :: JORDAN1K:9
theorem Th10: :: JORDAN1K:10
theorem Th11: :: JORDAN1K:11
theorem Th12: :: JORDAN1K:12
theorem Th13: :: JORDAN1K:13
theorem Th14: :: JORDAN1K:14
theorem :: JORDAN1K:15
theorem :: JORDAN1K:16
theorem :: JORDAN1K:17
theorem :: JORDAN1K:18
theorem :: JORDAN1K:19
theorem Th20: :: JORDAN1K:20
theorem Th21: :: JORDAN1K:21
theorem Th22: :: JORDAN1K:22
theorem Th23: :: JORDAN1K:23
theorem Th24: :: JORDAN1K:24
theorem Th25: :: JORDAN1K:25
theorem Th26: :: JORDAN1K:26
theorem Th27: :: JORDAN1K:27
theorem Th28: :: JORDAN1K:28
theorem Th29: :: JORDAN1K:29
theorem :: JORDAN1K:30
theorem Th31: :: JORDAN1K:31
theorem Th32: :: JORDAN1K:32
theorem Th33: :: JORDAN1K:33
theorem Th34: :: JORDAN1K:34
theorem Th35: :: JORDAN1K:35
theorem Th36: :: JORDAN1K:36
theorem :: JORDAN1K:37
definition
let n be
Element of
NAT ;
let A,
B be
Subset of
(TOP-REAL n);
func dist_min A,
B -> Real means :
Def1:
:: JORDAN1K:def 1
ex
A',
B' being
Subset of
(TopSpaceMetr (Euclid n)) st
(
A = A' &
B = B' &
it = min_dist_min A',
B' );
existence
ex b1 being Real ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & b1 = min_dist_min A',B' )
uniqueness
for b1, b2 being Real st ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & b1 = min_dist_min A',B' ) & ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & b2 = min_dist_min A',B' ) holds
b1 = b2
;
end;
:: deftheorem Def1 defines dist_min JORDAN1K:def 1 :
theorem Th38: :: JORDAN1K:38
theorem Th39: :: JORDAN1K:39
theorem Th40: :: JORDAN1K:40
theorem Th41: :: JORDAN1K:41
theorem Th42: :: JORDAN1K:42
theorem Th43: :: JORDAN1K:43
:: deftheorem defines dist JORDAN1K:def 2 :
theorem :: JORDAN1K:44
theorem :: JORDAN1K:45
theorem Th46: :: JORDAN1K:46
theorem :: JORDAN1K:47
theorem :: JORDAN1K:48
theorem :: JORDAN1K:49
theorem Th50: :: JORDAN1K:50
theorem :: JORDAN1K:51