Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-06 09:59 c82243a8

View on Github →

feat(analysis/normed_space): bounded linear maps with the operator norm form a normed space (closes #680)

Estimated changes

Modified src/analysis/normed_space/basic.lean

added structure normed_space.core

Created src/analysis/normed_space/operator_norm.lean

added theorem bounded_by_operator_norm

added theorem bounded_by_operator_norm_on_unit_ball

added theorem bounded_by_operator_norm_on_unit_vector

added def bounded_linear_maps

added theorem exists_bound'

added theorem exists_bound

added theorem ext

added theorem norm_of_unit_ball_bdd_above

added theorem operator_norm_bounded_by

added theorem operator_norm_homogeneous

added theorem operator_norm_nonneg

added theorem operator_norm_triangle

added theorem operator_norm_zero_iff

added theorem zero_in_im_ball

Modified src/order/conditionally_complete_lattice.lean

added theorem lattice.cSup_intro'