Mathlib v3 is deprecated. Go to Mathlib v4

Theorem controlled_closure_of_complete

Modification history

2023-01-19 07:18
src/analysis/normed/group/controlled_closure.lean
refactor(analysis/normed/group/hom): split (#18219) …
Modified controlled_closure_of_completeView on Github →
2022-07-24 16:34
src/analysis/normed/group/hom.lean
chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) …
Modified controlled_closure_of_completeView on Github →
2021-08-11 07:34
src/analysis/normed_space/normed_group_hom.lean
feat(analysis/normed_space): controlled surjectivity (#8498) …
Added controlled_closure_of_completeView on Github →