| changeset 61610 | 4f54d2759a0b |
| parent 61609 | 77b453bd616f |
| parent 61560 | 7c985fd653c5 |
| child 61711 | 21d7910d6816 |
| 61609:77b453bd616f | 61610:4f54d2759a0b |
|---|---|
1 section\<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close> |
1 section \<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close> |
2 |
2 |
3 theory Weierstrass |
3 theory Weierstrass |
4 imports Uniform_Limit Path_Connected |
4 imports Uniform_Limit Path_Connected |
5 |
|
6 begin |
5 begin |
7 |
6 |
8 (*Power.thy:*) |
7 (*Power.thy:*) |
9 declare power_divide [where b = "numeral w" for w, simp del] |
8 declare power_divide [where b = "numeral w" for w, simp del] |
10 |
9 |