Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-27 09:57 02ca4942

View on Github →

Remove outparam in normed space (#844)

Estimated changes

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

modified theorem is_bounded_linear_map.continuous

modified theorem is_bounded_linear_map.id

modified theorem is_bounded_linear_map.is_O_comp

modified theorem is_bounded_linear_map.is_O_id

modified theorem is_bounded_linear_map.is_O_sub

modified theorem is_bounded_linear_map.lim_zero_bounded_linear_map

modified theorem is_bounded_linear_map.neg

modified theorem is_bounded_linear_map.smul

modified theorem is_bounded_linear_map.sub

modified theorem is_bounded_linear_map.tendsto

modified def is_bounded_linear_map.to_linear_map

modified theorem is_bounded_linear_map.zero

modified structure is_bounded_linear_map

Modified src/analysis/normed_space/deriv.lean

modified theorem has_fderiv_at.is_o

modified theorem has_fderiv_at_filter_id

modified theorem has_fderiv_at_id

modified theorem has_fderiv_at_within_id

Modified src/analysis/normed_space/operator_norm.lean