Revision #1598 → #2647 · back to history
modifiedStone–Weierstrass theorem (real numbers)2b0f1d57cf8c
| Field | From #1598 | To #2647 |
|---|
| mathlib.decl | subalgebra_topologicalClosure_eq_top_of_separatesPoints | ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints |
| provenance | ai | ai-moderated |
modifiedStone–Weierstrass theorem (locally compact spaces)91e53e3ca61b
| Field | From #1598 | To #2647 |
|---|
| mathlib.decl | exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints | ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints |
| provenance | ai | ai-moderated |
modifiedPolynomial approximation in two variables9c6c45f1f35b
| Field | From #1598 | To #2647 |
|---|
| mathlib.decl | subalgebra_topologicalClosure_eq_top_of_separatesPoints | ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints |
| provenance | ai | ai-moderated |
modifiedApproximation by sums of products on X×Yf287c3b8ae46
| Field | From #1598 | To #2647 |
|---|
| mathlib.decl | subalgebra_topologicalClosure_eq_top_of_separatesPoints | ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints |
| provenance | ai | ai-moderated |
modifiedComplex unital *-algebra generated2a67a1039da0
| Field | From #1598 | To #2647 |
|---|
| mathlib.decl | StarSubalgebra.adjoin | StarAlgebra.adjoin |
| provenance | ai | ai-moderated |
modifiedLattice in C(X,R)aa6659c4a099
| Field | From #1598 | To #2647 |
|---|
| mathlib.decl | ContinuousMap.instLattice | ContinuousMap.instLatticeOfTopologicalLattice |
| provenance | ai | ai-moderated |