| 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 15524 | . 2 ⊢ ⇝ = {〈𝑓, 𝑦〉 ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))} | |
| 2 | 1 | relopabiv 5830 | 1 ⊢ Rel ⇝ |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 class class class wbr 5143 Rel wrel 5690 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 < clt 11295 − cmin 11492 ℤcz 12613 ℤ≥cuz 12878 ℝ+crp 13034 abscabs 15273 ⇝ cli 15520 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-opab 5206 df-xp 5691 df-rel 5692 df-clim 15524 |
| This theorem is referenced by: clim 15530 climcl 15535 climi 15546 climrlim2 15583 fclim 15589 climrecl 15619 climge0 15620 iserex 15693 caurcvg2 15714 caucvg 15715 iseralt 15721 fsumcvg3 15765 cvgcmpce 15854 climfsum 15856 climcnds 15887 trirecip 15899 ntrivcvgn0 15934 ovoliunlem1 25537 mbflimlem 25702 abelthlem5 26479 emcllem6 27044 lgamgulmlem4 27075 binomcxplemnn0 44368 binomcxplemnotnn0 44375 climf 45637 sumnnodd 45645 climf2 45681 climd 45687 clim2d 45688 climfv 45706 climuzlem 45758 climlimsup 45775 climlimsupcex 45784 climliminflimsupd 45816 climliminf 45821 liminflimsupclim 45822 xlimclimdm 45869 ioodvbdlimc1lem2 45947 ioodvbdlimc2lem 45949 stirlinglem12 46100 fouriersw 46246 |
| Copyright terms: Public domain | W3C validator |