Description: A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mopni.1 | β’ π½ = ( MetOpen β π· ) | |
Assertion | rnblopn | β’ ( ( π· β ( βMet β π ) β§ π΅ β ran ( ball β π· ) ) β π΅ β π½ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mopni.1 | β’ π½ = ( MetOpen β π· ) | |
2 | 1 | blssopn | β’ ( π· β ( βMet β π ) β ran ( ball β π· ) β π½ ) |
3 | 2 | sselda | β’ ( ( π· β ( βMet β π ) β§ π΅ β ran ( ball β π· ) ) β π΅ β π½ ) |