Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-29 14:48 b0aadaaa

View on Github →

cleanup(analysis/bounded_linear_maps): some reorganization

Estimated changes

Created analysis/bounded_linear_maps.lean

added theorem bounded_continuous_linear_map

added theorem is_bounded_linear_map.add

added theorem is_bounded_linear_map.comp

added theorem is_bounded_linear_map.continuous

added theorem is_bounded_linear_map.id

added theorem is_bounded_linear_map.lim_zero_bounded_linear_map

added theorem is_bounded_linear_map.neg

added theorem is_bounded_linear_map.smul

added theorem is_bounded_linear_map.sub

added theorem is_bounded_linear_map.tendsto

added theorem is_bounded_linear_map.zero

added structure is_bounded_linear_map

added theorem is_linear_map.with_bound

added theorem mul_inv_eq'

Deleted analysis/continuous_linear_maps.lean

deleted theorem bounded_continuous_linear_map

deleted theorem is_bounded_linear_map.add

deleted theorem is_bounded_linear_map.comp

deleted theorem is_bounded_linear_map.continuous

deleted theorem is_bounded_linear_map.id

deleted theorem is_bounded_linear_map.lim_zero_bounded_linear_map

deleted theorem is_bounded_linear_map.neg

deleted theorem is_bounded_linear_map.smul

deleted theorem is_bounded_linear_map.sub

deleted theorem is_bounded_linear_map.zero

deleted def is_bounded_linear_map

Modified analysis/metric_space.lean

added theorem exists_delta_of_continuous

Modified analysis/normed_space.lean

added theorem real.norm_eq_abs