Description: The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lpfval.1 | |- X = U. J |
|
Assertion | perflp | |- ( J e. Perf -> ( ( limPt ` J ) ` X ) = X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lpfval.1 | |- X = U. J |
|
2 | 1 | isperf | |- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) ) |
3 | 2 | simprbi | |- ( J e. Perf -> ( ( limPt ` J ) ` X ) = X ) |