Description: Closure of the distance function of a metric space. Part of Property M1 of Kreyszig p. 3. (Contributed by NM, 30-Aug-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | xmetcl | β’ ( ( π· β ( βMet β π ) β§ π΄ β π β§ π΅ β π ) β ( π΄ π· π΅ ) β β* ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xmetf | β’ ( π· β ( βMet β π ) β π· : ( π Γ π ) βΆ β* ) | |
2 | fovcdm | β’ ( ( π· : ( π Γ π ) βΆ β* β§ π΄ β π β§ π΅ β π ) β ( π΄ π· π΅ ) β β* ) | |
3 | 1 2 | syl3an1 | β’ ( ( π· β ( βMet β π ) β§ π΄ β π β§ π΅ β π ) β ( π΄ π· π΅ ) β β* ) |