Skip to content

Commit cac0cba

Browse files
feat: port Topology.ContinuousFunction.StoneWeierstrass (#4701)
1 parent d759934 commit cac0cba

File tree

2 files changed

+452
-0
lines changed

2 files changed

+452
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2594,6 +2594,7 @@ import Mathlib.Topology.ContinuousFunction.Compact
25942594
import Mathlib.Topology.ContinuousFunction.LocallyConstant
25952595
import Mathlib.Topology.ContinuousFunction.Ordered
25962596
import Mathlib.Topology.ContinuousFunction.Polynomial
2597+
import Mathlib.Topology.ContinuousFunction.StoneWeierstrass
25972598
import Mathlib.Topology.ContinuousFunction.T0Sierpinski
25982599
import Mathlib.Topology.ContinuousFunction.Weierstrass
25992600
import Mathlib.Topology.ContinuousOn

0 commit comments

Comments
 (0)