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

Definition df-lm 13775
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 (π‘₯ ∈ ℝ ↦ (sinβ€˜(Ο€ Β· π‘₯))) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.)
Assertion
Ref Expression
df-lm ⇝𝑑 = (𝑗 ∈ Top ↦ {βŸ¨π‘“, π‘₯⟩ ∣ (𝑓 ∈ (βˆͺ 𝑗 ↑pm β„‚) ∧ π‘₯ ∈ βˆͺ 𝑗 ∧ βˆ€π‘’ ∈ 𝑗 (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’))})
Distinct variable group:   𝑓,𝑗,π‘₯,𝑦,𝑒

Detailed syntax breakdown of Definition df-lm
StepHypRef Expression
1 clm 13772 . 2 class ⇝𝑑
2 vj . . 3 setvar 𝑗
3 ctop 13582 . . 3 class Top
4 vf . . . . . . 7 setvar 𝑓
54cv 1352 . . . . . 6 class 𝑓
62cv 1352 . . . . . . . 8 class 𝑗
76cuni 3811 . . . . . . 7 class βˆͺ 𝑗
8 cc 7811 . . . . . . 7 class β„‚
9 cpm 6651 . . . . . . 7 class ↑pm
107, 8, 9co 5877 . . . . . 6 class (βˆͺ 𝑗 ↑pm β„‚)
115, 10wcel 2148 . . . . 5 wff 𝑓 ∈ (βˆͺ 𝑗 ↑pm β„‚)
12 vx . . . . . . 7 setvar π‘₯
1312cv 1352 . . . . . 6 class π‘₯
1413, 7wcel 2148 . . . . 5 wff π‘₯ ∈ βˆͺ 𝑗
15 vu . . . . . . . 8 setvar 𝑒
1612, 15wel 2149 . . . . . . 7 wff π‘₯ ∈ 𝑒
17 vy . . . . . . . . . 10 setvar 𝑦
1817cv 1352 . . . . . . . . 9 class 𝑦
1915cv 1352 . . . . . . . . 9 class 𝑒
205, 18cres 4630 . . . . . . . . 9 class (𝑓 β†Ύ 𝑦)
2118, 19, 20wf 5214 . . . . . . . 8 wff (𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’
22 cuz 9530 . . . . . . . . 9 class β„€β‰₯
2322crn 4629 . . . . . . . 8 class ran β„€β‰₯
2421, 17, 23wrex 2456 . . . . . . 7 wff βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’
2516, 24wi 4 . . . . . 6 wff (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’)
2625, 15, 6wral 2455 . . . . 5 wff βˆ€π‘’ ∈ 𝑗 (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’)
2711, 14, 26w3a 978 . . . 4 wff (𝑓 ∈ (βˆͺ 𝑗 ↑pm β„‚) ∧ π‘₯ ∈ βˆͺ 𝑗 ∧ βˆ€π‘’ ∈ 𝑗 (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’))
2827, 4, 12copab 4065 . . 3 class {βŸ¨π‘“, π‘₯⟩ ∣ (𝑓 ∈ (βˆͺ 𝑗 ↑pm β„‚) ∧ π‘₯ ∈ βˆͺ 𝑗 ∧ βˆ€π‘’ ∈ 𝑗 (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’))}
292, 3, 28cmpt 4066 . 2 class (𝑗 ∈ Top ↦ {βŸ¨π‘“, π‘₯⟩ ∣ (𝑓 ∈ (βˆͺ 𝑗 ↑pm β„‚) ∧ π‘₯ ∈ βˆͺ 𝑗 ∧ βˆ€π‘’ ∈ 𝑗 (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’))})
301, 29wceq 1353 1 wff ⇝𝑑 = (𝑗 ∈ Top ↦ {βŸ¨π‘“, π‘₯⟩ ∣ (𝑓 ∈ (βˆͺ 𝑗 ↑pm β„‚) ∧ π‘₯ ∈ βˆͺ 𝑗 ∧ βˆ€π‘’ ∈ 𝑗 (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝑓 β†Ύ 𝑦):π‘¦βŸΆπ‘’))})
Colors of variables: wff set class
This definition is referenced by:  lmrcl  13776  lmfval  13777
  Copyright terms: Public domain W3C validator