Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-16 17:58 8e3d9cee

View on Github →

feat(measure_theory/continuous_map_dense): continuous functions are dense in Lp (#8306)

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.subgroup_of_range_eq_of_le

Created src/measure_theory/continuous_map_dense.lean

added theorem bounded_continuous_function.to_Lp_dense_range

added theorem continuous_map.to_Lp_dense_range

added theorem measure_theory.Lp.bounded_continuous_function_dense

Modified src/measure_theory/lp_space.lean

added theorem bounded_continuous_function.range_to_Lp

added theorem bounded_continuous_function.range_to_Lp_hom

added theorem continuous_map.range_to_Lp

added def measure_theory.Lp.bounded_continuous_function

added theorem measure_theory.Lp.mem_bounded_continuous_function_iff

Modified src/measure_theory/vitali_caratheodory.lean

Modified src/topology/algebra/group.lean

modified theorem subgroup.is_closed_topological_closure

modified theorem subgroup.subgroup_topological_closure

modified theorem subgroup.topological_closure_minimal