Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_linear_map.with_bound

Modification history

2018-08-29 14:48
analysis/bounded_linear_maps.lean
cleanup(analysis/bounded_linear_maps): some reorganization
Added is_linear_map.with_boundView on Github →