Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-29 17:54 bdf2d81e

View on Github →

feat(topology/continuous_function/stone_weierstrass): complex Stone-Weierstrass (#8012)

Estimated changes

Modified src/analysis/complex/basic.lean

added theorem complex.continuous_abs

added theorem complex.continuous_norm_sq

Modified src/topology/algebra/module.lean

added theorem submodule.topological_closure_map

added theorem submodule.topological_closure_mono

Modified src/topology/continuous_function/algebra.lean

Modified src/topology/continuous_function/bounded.lean

added theorem continuous_linear_map.comp_left_continuous_bounded_apply

Modified src/topology/continuous_function/compact.lean

added theorem continuous_linear_map.comp_left_continuous_compact_apply

added theorem continuous_linear_map.to_linear_comp_left_continuous_compact

added theorem continuous_map.linear_isometry_bounded_of_compact_apply_apply

added theorem continuous_map.linear_isometry_bounded_of_compact_symm_apply

Modified src/topology/continuous_function/stone_weierstrass.lean

added def continuous_map.conj_invariant_subalgebra

added theorem continuous_map.mem_conj_invariant_subalgebra

added theorem continuous_map.subalgebra_complex_topological_closure_eq_top_of_separates_points

added theorem subalgebra.separates_points.complex_to_real