Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-lm Unicode version

Definition df-lm 12561
 Description: Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.)
Assertion
Ref Expression
df-lm
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-lm
StepHypRef Expression
1 clm 12558 . 2
2 vj . . 3
3 ctop 12366 . . 3
4 vf . . . . . . 7
54cv 1334 . . . . . 6
62cv 1334 . . . . . . . 8
76cuni 3772 . . . . . . 7
8 cc 7724 . . . . . . 7
9 cpm 6591 . . . . . . 7
107, 8, 9co 5821 . . . . . 6
115, 10wcel 2128 . . . . 5
12 vx . . . . . . 7
1312cv 1334 . . . . . 6
1413, 7wcel 2128 . . . . 5
15 vu . . . . . . . 8
1612, 15wel 2129 . . . . . . 7
17 vy . . . . . . . . . 10
1817cv 1334 . . . . . . . . 9
1915cv 1334 . . . . . . . . 9
205, 18cres 4587 . . . . . . . . 9
2118, 19, 20wf 5165 . . . . . . . 8
22 cuz 9433 . . . . . . . . 9
2322crn 4586 . . . . . . . 8
2421, 17, 23wrex 2436 . . . . . . 7
2516, 24wi 4 . . . . . 6
2625, 15, 6wral 2435 . . . . 5
2711, 14, 26w3a 963 . . . 4
2827, 4, 12copab 4024 . . 3
292, 3, 28cmpt 4025 . 2
301, 29wceq 1335 1
 Colors of variables: wff set class This definition is referenced by:  lmrcl  12562  lmfval  12563
 Copyright terms: Public domain W3C validator