Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-28 19:37 4328cc3c

View on Github →

feat(topology/continuous_function): abstract statement of Weierstrass approximation (#7303)

Estimated changes

Modified src/algebra/algebra/subalgebra.lean

deleted theorem algebra.coe_top

added theorem algebra.top_to_submodule

added theorem algebra.top_to_subsemiring

added theorem subalgebra.coe_comap

added theorem subalgebra.mem_comap

Modified src/data/set_like.lean

Modified src/field_theory/normal.lean

Modified src/field_theory/splitting_field.lean

Modified src/linear_algebra/finite_dimensional.lean

Modified src/ring_theory/adjoin/basic.lean

Modified src/ring_theory/algebra_tower.lean

Modified src/topology/algebra/algebra.lean

added theorem subalgebra.topological_closure_coe

added theorem subalgebra.topological_closure_comap'_homeomorph

Modified src/topology/continuous_function/algebra.lean

modified theorem continuous_map.subsingleton_subalgebra

Modified src/topology/continuous_function/basic.lean

added theorem continuous_map.ext_iff

Modified src/topology/continuous_function/polynomial.lean

added theorem polynomial.aeval_continuous_map_apply

added def polynomial.to_continuous_map_alg_hom

added def polynomial.to_continuous_map_on_alg_hom

added theorem polynomial_functions.comap'_comp_right_alg_hom_Icc_homeo_I

added def polynomial_functions

added theorem polynomial_functions_coe

added theorem polynomial_functions_separates_points

Created src/topology/continuous_function/weierstrass.lean

added theorem continuous_map_mem_polynomial_functions_closure

added theorem exists_polynomial_near_continuous_map

added theorem exists_polynomial_near_of_continuous_on

added theorem polynomial_functions_closure_eq_top'

added theorem polynomial_functions_closure_eq_top