Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-29 14:48 21a93552

View on Github →

feat(analysis/continuous_linear_maps)

Estimated changes

Created analysis/continuous_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.zero

added def is_bounded_linear_map