Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-flimfrs Unicode version

Definition df-flimfrs 25682
 Description: Gives the limits of a function at a point relatively to a subspace of a topology . ( The condition ensures the traces of the neighborhoods of over is a filter ( see trnei 17603). The set can't be empty since its closure is not empty ( see cldifemp 25627). Experimental. (Contributed by FL, 15-Sep-2013.)
Assertion
Ref Expression
df-flimfrs t
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-flimfrs
StepHypRef Expression
1 cflimfrs 25681 . 2
2 vj . . 3
3 vk . . 3
4 ctop 16647 . . 3
5 va . . . 4
63cv 1631 . . . . . 6
76cuni 3843 . . . . 5
87cpw 3638 . . . 4
9 vp . . . . 5
10 vf . . . . 5
115cv 1631 . . . . . 6
12 ccl 16771 . . . . . . 7
136, 12cfv 5271 . . . . . 6
1411, 13cfv 5271 . . . . 5
152cv 1631 . . . . . . 7
1615cuni 3843 . . . . . 6
17 cmap 6788 . . . . . 6
1816, 11, 17co 5874 . . . . 5
1910cv 1631 . . . . . 6
209cv 1631 . . . . . . . . . 10
2120csn 3653 . . . . . . . . 9
22 cnei 16850 . . . . . . . . . 10
236, 22cfv 5271 . . . . . . . . 9
2421, 23cfv 5271 . . . . . . . 8
25 crest 13341 . . . . . . . 8 t
2624, 11, 25co 5874 . . . . . . 7 t
27 cflf 17646 . . . . . . 7
2815, 26, 27co 5874 . . . . . 6 t
2919, 28cfv 5271 . . . . 5 t
309, 10, 14, 18, 29cmpt2 5876 . . . 4 t
315, 8, 30cmpt 4093 . . 3 t
322, 3, 4, 4, 31cmpt2 5876 . 2 t
331, 32wceq 1632 1 t
 Colors of variables: wff set class This definition is referenced by:  islimrs  25683
 Copyright terms: Public domain W3C validator