Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stowei Structured version   Visualization version   GIF version

Theorem stowei 43654
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.)
Hypotheses
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 𝐸 ∈ ℝ+
Assertion
Ref Expression
stowei βˆƒπ‘“ ∈ 𝐴 βˆ€π‘‘ ∈ 𝑇 (absβ€˜((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸
Distinct variable groups:   𝑓,𝑔,𝑑,𝐴   𝑓,β„Ž,π‘Ÿ,π‘₯,𝑑,𝐴   𝑓,𝐸,𝑔,𝑑   𝑓,𝐹,𝑔,𝑑   𝑓,𝐽,π‘Ÿ,𝑑   𝑇,𝑓,𝑔,𝑑   β„Ž,𝐸,π‘Ÿ,π‘₯   β„Ž,𝐹,π‘Ÿ,π‘₯   𝑇,β„Ž,π‘Ÿ,π‘₯   𝑑,𝐾
Allowed substitution hints:   𝐢(π‘₯,𝑑,𝑓,𝑔,β„Ž,π‘Ÿ)   𝐽(π‘₯,𝑔,β„Ž)   𝐾(π‘₯,𝑓,𝑔,β„Ž,π‘Ÿ)

Proof of Theorem stowei
StepHypRef Expression
1 nfcv 2905 . . 3 Ⅎ𝑑𝐹
2 nftru 1804 . . 3 β„²π‘‘βŠ€
3 stowei.1 . . 3 𝐾 = (topGenβ€˜ran (,))
4 stowei.2 . . . 4 𝐽 ∈ Comp
54a1i 11 . . 3 (⊀ β†’ 𝐽 ∈ Comp)
6 stowei.3 . . 3 𝑇 = βˆͺ 𝐽
7 stowei.4 . . 3 𝐢 = (𝐽 Cn 𝐾)
8 stowei.5 . . . 4 𝐴 βŠ† 𝐢
98a1i 11 . . 3 (⊀ β†’ 𝐴 βŠ† 𝐢)
10 stowei.6 . . . 4 ((𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
11103adant1 1130 . . 3 ((⊀ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
12 stowei.7 . . . 4 ((𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
13123adant1 1130 . . 3 ((⊀ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
14 stowei.8 . . . 4 (π‘₯ ∈ ℝ β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴)
1514adantl 483 . . 3 ((⊀ ∧ π‘₯ ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴)
16 stowei.9 . . . 4 ((π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑) β†’ βˆƒβ„Ž ∈ 𝐴 (β„Žβ€˜π‘Ÿ) β‰  (β„Žβ€˜π‘‘))
1716adantl 483 . . 3 ((⊀ ∧ (π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑)) β†’ βˆƒβ„Ž ∈ 𝐴 (β„Žβ€˜π‘Ÿ) β‰  (β„Žβ€˜π‘‘))
18 stowei.10 . . . 4 𝐹 ∈ 𝐢
1918a1i 11 . . 3 (⊀ β†’ 𝐹 ∈ 𝐢)
20 stowei.11 . . . 4 𝐸 ∈ ℝ+
2120a1i 11 . . 3 (⊀ β†’ 𝐸 ∈ ℝ+)
221, 2, 3, 5, 6, 7, 9, 11, 13, 15, 17, 19, 21stoweid 43653 . 2 (⊀ β†’ βˆƒπ‘“ ∈ 𝐴 βˆ€π‘‘ ∈ 𝑇 (absβ€˜((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸)
2322mptru 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