WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Stone–Weierstrass theorem

Revision #2647 → #3186 · back to history

addedBernstein polynomial constructive proof9a973063b37d
modifiedLattice in C(X,R)aa6659c4a099
FieldFrom #2647To #3186
mathlib.moduleMathlib.Topology.ContinuousMap.LatticeMathlib.Topology.ContinuousMap.Ordered
noteThe lattice structure on `C(α, β)` (with sup/inf inherited pointwise) is provided; sub-lattice membership is then standard `Set` notion.The lattice structure on `C(α, β)` (with sup/inf inherited pointwise) is provided via `ContinuousMap.instLatticeOfTopologicalLattice` in `ContinuousMap.Ordered`.