Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-05 07:54 a7524b63

View on Github →

refactor(analysis/normed_space/operator_norm): topological modules (#1085)

refactor(analysis/normed_space/operator_norm): topological modules
remove useless typeclass in definition of topological module
refactor(analysis/normed_space/operator_norm): style

Estimated changes

Modified src/analysis/normed_space/basic.lean

deleted theorem continuous_smul

Modified src/analysis/normed_space/bounded_linear_maps.lean

deleted theorem bounded_linear_map.is_bounded_linear_map

deleted theorem bounded_linear_map.is_bounded_linear_map_comp_left

deleted theorem bounded_linear_map.is_bounded_linear_map_comp_right

added theorem continuous_linear_map.is_bounded_linear_map

added theorem continuous_linear_map.is_bounded_linear_map_comp_left

added theorem continuous_linear_map.is_bounded_linear_map_comp_right

added def is_bounded_bilinear_map.linear_deriv

added theorem is_bounded_bilinear_map_deriv_coe

deleted def is_bounded_linear_map.to_bounded_linear_map

added def is_bounded_linear_map.to_continuous_linear_map

deleted theorem is_linear_map.bounded_of_continuous_at

Modified src/analysis/normed_space/deriv.lean

Modified src/analysis/normed_space/operator_norm.lean

deleted theorem bounded_linear_map.add_apply

deleted theorem bounded_linear_map.bounds_bdd_below

deleted theorem bounded_linear_map.bounds_nonempty

deleted theorem bounded_linear_map.coe_add'

deleted theorem bounded_linear_map.coe_add

deleted theorem bounded_linear_map.coe_apply'

deleted theorem bounded_linear_map.coe_apply

deleted theorem bounded_linear_map.coe_coe

deleted theorem bounded_linear_map.coe_comp'

deleted theorem bounded_linear_map.coe_comp

deleted theorem bounded_linear_map.coe_id'

deleted theorem bounded_linear_map.coe_id

deleted theorem bounded_linear_map.coe_neg'

deleted theorem bounded_linear_map.coe_neg

deleted theorem bounded_linear_map.coe_sub'

deleted theorem bounded_linear_map.coe_sub

deleted theorem bounded_linear_map.coe_zero'

deleted theorem bounded_linear_map.coe_zero

deleted def bounded_linear_map.comp

deleted theorem bounded_linear_map.continuous

deleted theorem bounded_linear_map.ext

deleted theorem bounded_linear_map.ext_iff

deleted def bounded_linear_map.id

deleted theorem bounded_linear_map.id_apply

deleted theorem bounded_linear_map.is_O_comp

deleted theorem bounded_linear_map.is_O_id

deleted theorem bounded_linear_map.is_O_sub

deleted theorem bounded_linear_map.le_op_norm

deleted theorem bounded_linear_map.lipschitz

deleted theorem bounded_linear_map.map_add

deleted theorem bounded_linear_map.map_neg

deleted theorem bounded_linear_map.map_smul

deleted theorem bounded_linear_map.map_sub

deleted theorem bounded_linear_map.map_zero

deleted theorem bounded_linear_map.neg_apply

deleted def bounded_linear_map.op_norm

deleted theorem bounded_linear_map.op_norm_comp_le

deleted theorem bounded_linear_map.op_norm_le_bound

deleted theorem bounded_linear_map.op_norm_nonneg

deleted theorem bounded_linear_map.op_norm_smul

deleted theorem bounded_linear_map.op_norm_triangle

deleted theorem bounded_linear_map.op_norm_zero_iff

deleted def bounded_linear_map.prod

deleted theorem bounded_linear_map.ratio_le_op_norm

deleted def bounded_linear_map.scalar_prod_space_iso

deleted theorem bounded_linear_map.smul_apply

deleted theorem bounded_linear_map.sub_apply

deleted theorem bounded_linear_map.unit_le_op_norm

deleted def bounded_linear_map.zero

deleted theorem bounded_linear_map.zero_apply

deleted structure bounded_linear_map

added theorem continuous_linear_map.bound

added theorem continuous_linear_map.bounds_bdd_below

added theorem continuous_linear_map.bounds_nonempty

added theorem continuous_linear_map.is_O_comp

added theorem continuous_linear_map.is_O_id

added theorem continuous_linear_map.is_O_sub

added theorem continuous_linear_map.le_op_norm

added theorem continuous_linear_map.lipschitz

added theorem continuous_linear_map.norm_id

added theorem continuous_linear_map.norm_zero

added def continuous_linear_map.op_norm

added theorem continuous_linear_map.op_norm_comp_le

added theorem continuous_linear_map.op_norm_le_bound

added theorem continuous_linear_map.op_norm_nonneg

added theorem continuous_linear_map.op_norm_smul

added theorem continuous_linear_map.op_norm_triangle

added theorem continuous_linear_map.op_norm_zero_iff

added theorem continuous_linear_map.ratio_le_op_norm

added theorem continuous_linear_map.scalar_prod_space_iso_norm

added theorem continuous_linear_map.unit_le_op_norm

added theorem linear_map.continuous_of_bound

added def linear_map.with_bound

added theorem linear_map_with_bound_apply

added theorem linear_map_with_bound_coe

Created src/topology/algebra/module.lean

added theorem continuous_linear_map.add_apply

added theorem continuous_linear_map.coe_add'

added theorem continuous_linear_map.coe_add

added theorem continuous_linear_map.coe_apply'

added theorem continuous_linear_map.coe_apply

added theorem continuous_linear_map.coe_coe

added theorem continuous_linear_map.coe_comp'

added theorem continuous_linear_map.coe_comp

added theorem continuous_linear_map.coe_id'

added theorem continuous_linear_map.coe_id

added theorem continuous_linear_map.coe_neg'

added theorem continuous_linear_map.coe_neg

added theorem continuous_linear_map.coe_sub'

added theorem continuous_linear_map.coe_sub

added theorem continuous_linear_map.coe_zero'

added theorem continuous_linear_map.coe_zero

added def continuous_linear_map.comp

added theorem continuous_linear_map.ext

added theorem continuous_linear_map.ext_iff

added def continuous_linear_map.id

added theorem continuous_linear_map.id_apply

added theorem continuous_linear_map.map_add

added theorem continuous_linear_map.map_neg

added theorem continuous_linear_map.map_smul

added theorem continuous_linear_map.map_sub

added theorem continuous_linear_map.map_zero

added theorem continuous_linear_map.neg_apply

added def continuous_linear_map.prod

added def continuous_linear_map.scalar_prod_space_iso

added theorem continuous_linear_map.smul_apply

added theorem continuous_linear_map.sub_apply

added def continuous_linear_map.zero

added theorem continuous_linear_map.zero_apply

added structure continuous_linear_map

added theorem continuous_smul'

added theorem continuous_smul