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

Definition df-lm 12984
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 12981 . 2 class 𝑡
2 vj . . 3 setvar 𝑗
3 ctop 12789 . . 3 class Top
4 vf . . . . . . 7 setvar 𝑓
54cv 1347 . . . . . 6 class 𝑓
62cv 1347 . . . . . . . 8 class 𝑗
76cuni 3796 . . . . . . 7 class 𝑗
8 cc 7772 . . . . . . 7 class
9 cpm 6627 . . . . . . 7 class pm
107, 8, 9co 5853 . . . . . 6 class ( 𝑗pm ℂ)
115, 10wcel 2141 . . . . 5 wff 𝑓 ∈ ( 𝑗pm ℂ)
12 vx . . . . . . 7 setvar 𝑥
1312cv 1347 . . . . . 6 class 𝑥
1413, 7wcel 2141 . . . . 5 wff 𝑥 𝑗
15 vu . . . . . . . 8 setvar 𝑢
1612, 15wel 2142 . . . . . . 7 wff 𝑥𝑢
17 vy . . . . . . . . . 10 setvar 𝑦
1817cv 1347 . . . . . . . . 9 class 𝑦
1915cv 1347 . . . . . . . . 9 class 𝑢
205, 18cres 4613 . . . . . . . . 9 class (𝑓𝑦)
2118, 19, 20wf 5194 . . . . . . . 8 wff (𝑓𝑦):𝑦𝑢
22 cuz 9487 . . . . . . . . 9 class
2322crn 4612 . . . . . . . 8 class ran ℤ
2421, 17, 23wrex 2449 . . . . . . 7 wff 𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢
2516, 24wi 4 . . . . . 6 wff (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2625, 15, 6wral 2448 . . . . 5 wff 𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2711, 14, 26w3a 973 . . . 4 wff (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))
2827, 4, 12copab 4049 . . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))}
292, 3, 28cmpt 4050 . 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
301, 29wceq 1348 1 wff 𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Colors of variables: wff set class
This definition is referenced by:  lmrcl  12985  lmfval  12986
  Copyright terms: Public domain W3C validator