changeset 69517 | dc20f278e8f3 |
parent 69508 | 2a4c8a2a3f8e |
child 69597 | ff784d5a5bfb |
69516:09bb8f470959 | 69517:dc20f278e8f3 |
---|---|
1 section \<open>The Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close> |
1 section \<open>Bernstein-Weierstrass and Stone-Weierstrass\<close> |
2 |
2 |
3 text\<open>By L C Paulson (2015)\<close> |
3 text\<open>By L C Paulson (2015)\<close> |
4 |
4 |
5 theory Weierstrass_Theorems |
5 theory Weierstrass_Theorems |
6 imports Uniform_Limit Path_Connected Derivative |
6 imports Uniform_Limit Path_Connected Derivative |