Commit 2023-06-05 20:15 cac0cba2

View on Github →

feat: port Topology.ContinuousFunction.StoneWeierstrass (#4701)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean

added def ContinuousMap.ConjInvariantSubalgebra

added theorem ContinuousMap.abs_mem_subalgebra_closure

added def ContinuousMap.attachBound

added theorem ContinuousMap.attachBound_apply_coe

added theorem ContinuousMap.comp_attachBound_mem_closure

added theorem ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints

added theorem ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints

added theorem ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints

added theorem ContinuousMap.inf_mem_closed_subalgebra

added theorem ContinuousMap.inf_mem_subalgebra_closure

added theorem ContinuousMap.mem_conjInvariantSubalgebra

added theorem ContinuousMap.polynomial_comp_attachBound

added theorem ContinuousMap.polynomial_comp_attachBound_mem

added theorem ContinuousMap.subalgebraConjInvariant

added theorem ContinuousMap.subalgebra_isROrC_topologicalClosure_eq_top_of_separatesPoints

added theorem ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints

added theorem ContinuousMap.sublattice_closure_eq_top

added theorem ContinuousMap.sup_mem_closed_subalgebra

added theorem ContinuousMap.sup_mem_subalgebra_closure

added theorem Subalgebra.SeparatesPoints.isROrC_to_real