Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-06 16:14 ae8a1fb6

View on Github →

refactor(analysis/normed_space/bounded_linear_maps): nondiscrete normed field

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

added theorem bdd_above_range_norm_image_div_norm

deleted theorem bounded_by_operator_norm_on_unit_ball

deleted theorem bounded_by_operator_norm_on_unit_vector

added theorem bounded_linear_maps.coe_zero

added theorem bounded_linear_maps.map_zero

added theorem bounded_linear_maps.one_smul

added theorem bounded_linear_maps.smul_coe

added theorem bounded_linear_maps.zero_smul

deleted theorem exists_bound'

modified theorem exists_bound

deleted theorem norm_of_unit_ball_bdd_above

modified theorem operator_norm_bounded_by

modified theorem operator_norm_homogeneous

added theorem operator_norm_homogeneous_le

modified theorem operator_norm_triangle

added def to_linear_map

deleted theorem zero_in_im_ball