Description: A filter contains all of the neighborhoods of its limit points. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Mario Carneiro, 9-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | flimnei | |- ( ( A e. ( J fLim F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> N e. F ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flimneiss | |- ( A e. ( J fLim F ) -> ( ( nei ` J ) ` { A } ) C_ F ) |
|
2 | 1 | sselda | |- ( ( A e. ( J fLim F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> N e. F ) |