Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > climrel | Structured version Visualization version GIF version |
Description: The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
Ref | Expression |
---|---|
climrel | ⊢ Rel ⇝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clim 14833 | . 2 ⊢ ⇝ = {〈𝑓, 𝑦〉 ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))} | |
2 | 1 | relopabi 5687 | 1 ⊢ Rel ⇝ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∈ wcel 2105 ∀wral 3135 ∃wrex 3136 class class class wbr 5057 Rel wrel 5553 ‘cfv 6348 (class class class)co 7145 ℂcc 10523 < clt 10663 − cmin 10858 ℤcz 11969 ℤ≥cuz 12231 ℝ+crp 12377 abscabs 14581 ⇝ cli 14829 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-opab 5120 df-xp 5554 df-rel 5555 df-clim 14833 |
This theorem is referenced by: clim 14839 climcl 14844 climi 14855 climrlim2 14892 fclim 14898 climrecl 14928 climge0 14929 iserex 15001 caurcvg2 15022 caucvg 15023 iseralt 15029 fsumcvg3 15074 cvgcmpce 15161 climfsum 15163 climcnds 15194 trirecip 15206 ntrivcvgn0 15242 ovoliunlem1 24030 mbflimlem 24195 abelthlem5 24950 emcllem6 25505 lgamgulmlem4 25536 binomcxplemnn0 40558 binomcxplemnotnn0 40565 climf 41779 sumnnodd 41787 climf2 41823 climd 41829 clim2d 41830 climfv 41848 climuzlem 41900 climlimsup 41917 climlimsupcex 41926 climliminflimsupd 41958 climliminf 41963 liminflimsupclim 41964 xlimclimdm 42011 ioodvbdlimc1lem2 42093 ioodvbdlimc2lem 42095 stirlinglem12 42247 fouriersw 42393 |
Copyright terms: Public domain | W3C validator |