Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-25 18:58 038f809c

View on Github →

refactor(analysis/normed_space/operator_norm): replace subspace with … (#955)

refactor(analysis/normed_space/operator_norm): replace subspace with structure
refactor(analysis/normed_space/operator_norm): add coercions

Estimated changes

Modified src/analysis/normed_space/bounded_linear_maps.lean

added theorem bounded_linear_map.is_bounded_linear_map

added def is_bounded_linear_map.to_bounded_linear_map

deleted theorem mul_inv_eq'

Modified src/analysis/normed_space/operator_norm.lean

added theorem bounded_linear_map.add_apply

added theorem bounded_linear_map.coe_add'

added theorem bounded_linear_map.coe_add

added theorem bounded_linear_map.coe_apply'

added theorem bounded_linear_map.coe_apply

added theorem bounded_linear_map.coe_coe

added theorem bounded_linear_map.coe_comp'

added theorem bounded_linear_map.coe_comp

added theorem bounded_linear_map.coe_id'

added theorem bounded_linear_map.coe_id

added theorem bounded_linear_map.coe_neg'

added theorem bounded_linear_map.coe_neg

added theorem bounded_linear_map.coe_sub'

added theorem bounded_linear_map.coe_sub

added theorem bounded_linear_map.coe_zero'

modified theorem bounded_linear_map.coe_zero

added theorem bounded_linear_map.continuous

added def bounded_linear_map.id

added theorem bounded_linear_map.id_apply

modified theorem bounded_linear_map.is_O_sub

modified theorem bounded_linear_map.neg_apply

deleted theorem bounded_linear_map.one_smul

added theorem bounded_linear_map.sub_apply

deleted theorem bounded_linear_map.tendsto

deleted def bounded_linear_map.to_linear_map

added def bounded_linear_map.zero

deleted theorem bounded_linear_map.zero_smul

added structure bounded_linear_map

deleted def bounded_linear_map

deleted def bounded_linear_map_subspace

added theorem exists_pos_bound_of_bound

deleted def is_bounded_linear_map.to_bounded_linear_map