Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-04 15:28 585e107f

View on Github →

feat(topology/algebra/module): continuous linear equiv (#1839)

feat(topology/algebra/module): continuous linear equiv
linting
reviewer's comments

Estimated changes

Modified src/analysis/calculus/fderiv.lean

added theorem has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv

Modified src/analysis/normed_space/banach.lean

modified theorem linear_equiv.is_bounded_inv

added def linear_equiv.to_continuous_linear_equiv_of_continuous

Modified src/analysis/normed_space/finite_dimension.lean

added def linear_equiv.to_continuous_linear_equiv

added def linear_map.to_continuous_linear_map

Modified src/analysis/normed_space/operator_norm.lean

Modified src/topology/algebra/module.lean

modified theorem continuous.smul

added theorem continuous_linear_equiv.apply_symm_apply

added theorem continuous_linear_equiv.coe_apply

added theorem continuous_linear_equiv.coe_coe

added theorem continuous_linear_equiv.ext

added theorem continuous_linear_equiv.map_add

added theorem continuous_linear_equiv.map_neg

added theorem continuous_linear_equiv.map_smul

added theorem continuous_linear_equiv.map_sub

added theorem continuous_linear_equiv.map_zero

added theorem continuous_linear_equiv.symm_apply_apply

added theorem continuous_linear_equiv.symm_to_linear_equiv

added def continuous_linear_equiv.to_continuous_linear_map

added def continuous_linear_equiv.to_homeomorph

added theorem continuous_linear_equiv.trans_to_linear_equiv

added structure continuous_linear_equiv

modified theorem continuous_linear_map.add_comp

modified theorem continuous_linear_map.coe_add'

modified theorem continuous_linear_map.coe_add

modified theorem continuous_linear_map.coe_apply'

modified theorem continuous_linear_map.coe_apply

modified theorem continuous_linear_map.coe_coe

modified theorem continuous_linear_map.coe_comp'

modified theorem continuous_linear_map.coe_comp

modified theorem continuous_linear_map.coe_id'

modified theorem continuous_linear_map.coe_id

modified theorem continuous_linear_map.coe_neg'

modified theorem continuous_linear_map.coe_neg

modified theorem continuous_linear_map.coe_sub'

modified theorem continuous_linear_map.coe_sub

modified theorem continuous_linear_map.coe_zero'

modified theorem continuous_linear_map.coe_zero

modified def continuous_linear_map.comp

modified theorem continuous_linear_map.comp_add

modified theorem continuous_linear_map.comp_zero

modified theorem continuous_linear_map.ext

modified theorem continuous_linear_map.ext_iff

modified def continuous_linear_map.id

modified theorem continuous_linear_map.id_apply

modified theorem continuous_linear_map.map_zero

modified theorem continuous_linear_map.one_apply

modified def continuous_linear_map.prod

modified def continuous_linear_map.smul_right

modified theorem continuous_linear_map.smul_right_apply

modified theorem continuous_linear_map.smul_right_one_eq_iff

modified theorem continuous_linear_map.smul_right_one_one

modified theorem continuous_linear_map.sub_apply

modified def continuous_linear_map.zero

modified theorem continuous_linear_map.zero_apply

modified theorem continuous_linear_map.zero_comp

modified theorem continuous_smul

modified theorem is_closed_map_smul_of_ne_zero

modified theorem is_closed_map_smul_of_unit

modified theorem is_open_map_smul_of_ne_zero

modified theorem is_open_map_smul_of_unit

modified def topological_vector_space