Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > stowei | Structured version Visualization version GIF version |
Description: This theorem proves the Stone-Weierstrass theorem for real-valued functions: let π½ be a compact topology on π, and πΆ be the set of real continuous functions on π. Assume that π΄ is a subalgebra of πΆ (closed under addition and multiplication of functions) containing constant functions and discriminating points (if π and π‘ are distinct points in π, then there exists a function β in π΄ such that h(r) is distinct from h(t) ). Then, for any continuous function πΉ and for any positive real πΈ, there exists a function π in the subalgebra π΄, such that π approximates πΉ up to πΈ (πΈ represents the usual Ξ΅ value). As a classical example, given any a, b reals, the closed interval π = [π, π] could be taken, along with the subalgebra π΄ of real polynomials on π, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [π, π]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 43653: often times it will be better to use stoweid 43653 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Ref | Expression |
---|---|
stowei.1 | β’ πΎ = (topGenβran (,)) |
stowei.2 | β’ π½ β Comp |
stowei.3 | β’ π = βͺ π½ |
stowei.4 | β’ πΆ = (π½ Cn πΎ) |
stowei.5 | β’ π΄ β πΆ |
stowei.6 | β’ ((π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
stowei.7 | β’ ((π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
stowei.8 | β’ (π₯ β β β (π‘ β π β¦ π₯) β π΄) |
stowei.9 | β’ ((π β π β§ π‘ β π β§ π β π‘) β ββ β π΄ (ββπ) β (ββπ‘)) |
stowei.10 | β’ πΉ β πΆ |
stowei.11 | β’ πΈ β β+ |
Ref | Expression |
---|---|
stowei | β’ βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2905 | . . 3 β’ β²π‘πΉ | |
2 | nftru 1804 | . . 3 β’ β²π‘β€ | |
3 | stowei.1 | . . 3 β’ πΎ = (topGenβran (,)) | |
4 | stowei.2 | . . . 4 β’ π½ β Comp | |
5 | 4 | a1i 11 | . . 3 β’ (β€ β π½ β Comp) |
6 | stowei.3 | . . 3 β’ π = βͺ π½ | |
7 | stowei.4 | . . 3 β’ πΆ = (π½ Cn πΎ) | |
8 | stowei.5 | . . . 4 β’ π΄ β πΆ | |
9 | 8 | a1i 11 | . . 3 β’ (β€ β π΄ β πΆ) |
10 | stowei.6 | . . . 4 β’ ((π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) | |
11 | 10 | 3adant1 1130 | . . 3 β’ ((β€ β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
12 | stowei.7 | . . . 4 β’ ((π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) | |
13 | 12 | 3adant1 1130 | . . 3 β’ ((β€ β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
14 | stowei.8 | . . . 4 β’ (π₯ β β β (π‘ β π β¦ π₯) β π΄) | |
15 | 14 | adantl 483 | . . 3 β’ ((β€ β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
16 | stowei.9 | . . . 4 β’ ((π β π β§ π‘ β π β§ π β π‘) β ββ β π΄ (ββπ) β (ββπ‘)) | |
17 | 16 | adantl 483 | . . 3 β’ ((β€ β§ (π β π β§ π‘ β π β§ π β π‘)) β ββ β π΄ (ββπ) β (ββπ‘)) |
18 | stowei.10 | . . . 4 β’ πΉ β πΆ | |
19 | 18 | a1i 11 | . . 3 β’ (β€ β πΉ β πΆ) |
20 | stowei.11 | . . . 4 β’ πΈ β β+ | |
21 | 20 | a1i 11 | . . 3 β’ (β€ β πΈ β β+) |
22 | 1, 2, 3, 5, 6, 7, 9, 11, 13, 15, 17, 19, 21 | stoweid 43653 | . 2 β’ (β€ β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) |
23 | 22 | mptru 1546 | 1 β’ βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 397 β§ w3a 1087 = wceq 1539 β€wtru 1540 β wcel 2104 β wne 2941 βwral 3062 βwrex 3071 β wss 3893 βͺ cuni 4845 class class class wbr 5082 β¦ cmpt 5165 ran crn 5598 βcfv 6455 (class class class)co 7304 βcr 10913 + caddc 10917 Β· cmul 10919 < clt 11052 β cmin 11248 β+crp 12773 (,)cioo 13122 abscabs 14987 topGenctg 17190 Cn ccn 22417 Compccmp 22579 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-rep 5219 ax-sep 5233 ax-nul 5240 ax-pow 5298 ax-pr 5362 ax-un 7617 ax-inf2 9440 ax-cnex 10970 ax-resscn 10971 ax-1cn 10972 ax-icn 10973 ax-addcl 10974 ax-addrcl 10975 ax-mulcl 10976 ax-mulrcl 10977 ax-mulcom 10978 ax-addass 10979 ax-mulass 10980 ax-distr 10981 ax-i2m1 10982 ax-1ne0 10983 ax-1rid 10984 ax-rnegex 10985 ax-rrecex 10986 ax-cnre 10987 ax-pre-lttri 10988 ax-pre-lttrn 10989 ax-pre-ltadd 10990 ax-pre-mulgt0 10991 ax-pre-sup 10992 ax-addf 10993 ax-mulf 10994 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3278 df-reu 3279 df-rab 3280 df-v 3440 df-sbc 3723 df-csb 3839 df-dif 3896 df-un 3898 df-in 3900 df-ss 3910 df-pss 3912 df-nul 4264 df-if 4467 df-pw 4542 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4846 df-int 4888 df-iun 4934 df-iin 4935 df-br 5083 df-opab 5145 df-mpt 5166 df-tr 5200 df-id 5497 df-eprel 5503 df-po 5511 df-so 5512 df-fr 5552 df-se 5553 df-we 5554 df-xp 5603 df-rel 5604 df-cnv 5605 df-co 5606 df-dm 5607 df-rn 5608 df-res 5609 df-ima 5610 df-pred 6214 df-ord 6281 df-on 6282 df-lim 6283 df-suc 6284 df-iota 6407 df-fun 6457 df-fn 6458 df-f 6459 df-f1 6460 df-fo 6461 df-f1o 6462 df-fv 6463 df-isom 6464 df-riota 7261 df-ov 7307 df-oprab 7308 df-mpo 7309 df-of 7562 df-om 7742 df-1st 7860 df-2nd 7861 df-supp 8006 df-frecs 8125 df-wrecs 8156 df-recs 8230 df-rdg 8269 df-1o 8325 df-2o 8326 df-er 8526 df-map 8645 df-pm 8646 df-ixp 8714 df-en 8762 df-dom 8763 df-sdom 8764 df-fin 8765 df-fsupp 9170 df-fi 9211 df-sup 9242 df-inf 9243 df-oi 9310 df-card 9738 df-pnf 11054 df-mnf 11055 df-xr 11056 df-ltxr 11057 df-le 11058 df-sub 11250 df-neg 11251 df-div 11676 df-nn 12017 df-2 12079 df-3 12080 df-4 12081 df-5 12082 df-6 12083 df-7 12084 df-8 12085 df-9 12086 df-n0 12277 df-z 12363 df-dec 12481 df-uz 12626 df-q 12732 df-rp 12774 df-xneg 12891 df-xadd 12892 df-xmul 12893 df-ioo 13126 df-ioc 13127 df-ico 13128 df-icc 13129 df-fz 13283 df-fzo 13426 df-fl 13555 df-seq 13765 df-exp 13826 df-hash 14088 df-cj 14852 df-re 14853 df-im 14854 df-sqrt 14988 df-abs 14989 df-clim 15239 df-rlim 15240 df-sum 15440 df-struct 16890 df-sets 16907 df-slot 16925 df-ndx 16937 df-base 16955 df-ress 16984 df-plusg 17017 df-mulr 17018 df-starv 17019 df-sca 17020 df-vsca 17021 df-ip 17022 df-tset 17023 df-ple 17024 df-ds 17026 df-unif 17027 df-hom 17028 df-cco 17029 df-rest 17175 df-topn 17176 df-0g 17194 df-gsum 17195 df-topgen 17196 df-pt 17197 df-prds 17200 df-xrs 17255 df-qtop 17260 df-imas 17261 df-xps 17263 df-mre 17337 df-mrc 17338 df-acs 17340 df-mgm 18368 df-sgrp 18417 df-mnd 18428 df-submnd 18473 df-mulg 18743 df-cntz 18965 df-cmn 19430 df-psmet 20631 df-xmet 20632 df-met 20633 df-bl 20634 df-mopn 20635 df-cnfld 20640 df-top 22085 df-topon 22102 df-topsp 22124 df-bases 22138 df-cld 22212 df-cn 22420 df-cnp 22421 df-cmp 22580 df-tx 22755 df-hmeo 22948 df-xms 23515 df-ms 23516 df-tms 23517 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |