Commit 2019-04-26 20:52 53f98786
View on Github →refactor(analysis/normed_space): use bundled type for fderiv
(#956)
- feat(analysis/normed_space): refactor fderiv to use bounded_linear_map
- uniqueness remains sorry'd
- more simp lemmas about bounded_linear_map
- refactor uniqueness proof
- fix(analysis/normed_space/operator_norm): rename
bound_le_op_norm
toop_norm_le_bound
- so that the inequality goes the correct way.