Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-11 07:34 1d4400c1

View on Github →

feat(analysis/normed_space): controlled surjectivity (#8498) From LTE.

Estimated changes

Modified src/analysis/normed_space/normed_group_hom.lean

added theorem controlled_closure_of_complete

added theorem controlled_closure_range_of_complete

added theorem normed_group_hom.op_norm_eq_of_bounds

added theorem normed_group_hom.surjective_on_with.surj_on

added def normed_group_hom.surjective_on_with