Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-15 22:29 cc48a5a4

View on Github →

feat(geometry/manifold/diffeomorph): expand API (#6668)

Estimated changes

Modified src/geometry/manifold/diffeomorph.lean

added theorem continuous_linear_equiv.coe_to_diffeomorph

added theorem continuous_linear_equiv.coe_to_diffeomorph_symm

added theorem continuous_linear_equiv.symm_to_diffeomorph

added def continuous_linear_equiv.to_diffeomorph

added theorem diffeomorph.apply_symm_apply

added theorem diffeomorph.coe_coe

added theorem diffeomorph.coe_fn_injective

added theorem diffeomorph.coe_refl

added theorem diffeomorph.coe_to_equiv

added theorem diffeomorph.coe_to_homeomorph

added theorem diffeomorph.coe_to_homeomorph_symm

added theorem diffeomorph.coe_trans

added theorem diffeomorph.ext

added theorem diffeomorph.image_eq_preimage

added theorem diffeomorph.image_symm_image

added theorem diffeomorph.range_comp

added theorem diffeomorph.refl_to_equiv

added theorem diffeomorph.refl_trans

added theorem diffeomorph.smooth_trans_diffeomorph_left

added theorem diffeomorph.smooth_trans_diffeomorph_right

added theorem diffeomorph.symm_apply_apply

added theorem diffeomorph.symm_image_eq_preimage

added theorem diffeomorph.symm_image_image

added theorem diffeomorph.symm_refl

added theorem diffeomorph.symm_to_equiv

added theorem diffeomorph.symm_to_homeomorph

added theorem diffeomorph.symm_trans'

added theorem diffeomorph.symm_trans

added theorem diffeomorph.times_cont_mdiff_at_comp_diffeomorph_iff

added theorem diffeomorph.times_cont_mdiff_at_diffeomorph_comp_iff

added theorem diffeomorph.times_cont_mdiff_at_trans_diffeomorph_left

added theorem diffeomorph.times_cont_mdiff_at_trans_diffeomorph_right

added theorem diffeomorph.times_cont_mdiff_comp_diffeomorph_iff

added theorem diffeomorph.times_cont_mdiff_diffeomorph_comp_iff

added theorem diffeomorph.times_cont_mdiff_on_comp_diffeomorph_iff

added theorem diffeomorph.times_cont_mdiff_on_diffeomorph_comp_iff

added theorem diffeomorph.times_cont_mdiff_on_trans_diffeomorph_left

added theorem diffeomorph.times_cont_mdiff_on_trans_diffeomorph_right

added theorem diffeomorph.times_cont_mdiff_trans_diffeomorph_left

added theorem diffeomorph.times_cont_mdiff_trans_diffeomorph_right

added theorem diffeomorph.times_cont_mdiff_within_at_comp_diffeomorph_iff

added theorem diffeomorph.times_cont_mdiff_within_at_diffeomorph_comp_iff

added theorem diffeomorph.times_cont_mdiff_within_at_trans_diffeomorph_left

added theorem diffeomorph.times_cont_mdiff_within_at_trans_diffeomorph_right

added theorem diffeomorph.to_equiv_coe_symm

added theorem diffeomorph.to_equiv_inj

added theorem diffeomorph.to_equiv_injective

added def diffeomorph.to_homeomorph

added theorem diffeomorph.to_homeomorph_to_equiv

added theorem diffeomorph.to_local_homeomorph_mdifferentiable

added def diffeomorph.to_trans_diffeomorph

added theorem diffeomorph.trans_refl

added theorem diffeomorph.trans_symm

added theorem diffeomorph.unique_diff_on_image

added theorem diffeomorph.unique_diff_on_preimage

added theorem diffeomorph.unique_mdiff_on_image

added theorem diffeomorph.unique_mdiff_on_image_aux

added theorem diffeomorph.unique_mdiff_on_preimage

added structure diffeomorph

deleted def diffeomorph

added theorem model_with_corners.coe_ext_chart_at_trans_diffeomorph

added theorem model_with_corners.coe_ext_chart_at_trans_diffeomorph_symm

added theorem model_with_corners.coe_trans_diffeomorph

added theorem model_with_corners.coe_trans_diffeomorph_symm

added theorem model_with_corners.ext_chart_at_trans_diffeomorph_target

added def model_with_corners.trans_diffeomorph

added theorem model_with_corners.trans_diffeomorph_range

deleted theorem times_diffeomorph.coe_eq_to_equiv

deleted structure times_diffeomorph

Modified src/geometry/manifold/times_cont_mdiff.lean

added theorem times_cont_mdiff_at.comp_times_cont_mdiff_within_at