Mathlib Changelog
Changelog
About
Github
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