Commit 2023-11-30 19:19 4ff17db0

View on Github →

chore: split Geometry/Manifold/ContMDiff (#8726) At about 2200 lines, this is currently the longest file in the Geometry/Manifolds. (It also moves the slowly compiling proof of ContMDiffWithinAt.cle_arrowCongr out of a common recompilation path.)

Estimated changes

deleted theorem ContDiff.comp_contMDiff
deleted theorem ContDiff.comp_contMDiffAt
deleted theorem ContMDiff.cle_arrowCongr
deleted theorem ContMDiff.clm_apply
deleted theorem ContMDiff.clm_comp
deleted theorem ContMDiff.clm_postcomp
deleted theorem ContMDiff.clm_precomp
deleted theorem ContMDiff.clm_prodMap
deleted theorem ContMDiff.comp
deleted theorem ContMDiff.contMDiffAt
deleted theorem ContMDiff.contMDiffOn
deleted theorem ContMDiff.continuous
deleted theorem ContMDiff.fst
deleted theorem ContMDiff.of_le
deleted theorem ContMDiff.of_succ
deleted theorem ContMDiff.prod_map
deleted theorem ContMDiff.prod_mk_space
deleted theorem ContMDiff.smooth
deleted theorem ContMDiff.smul
deleted theorem ContMDiff.snd
deleted def ContMDiff
deleted theorem ContMDiffAt.clm_comp
deleted theorem ContMDiffAt.comp_of_eq
deleted theorem ContMDiffAt.continuousAt
deleted theorem ContMDiffAt.fst
deleted theorem ContMDiffAt.of_le
deleted theorem ContMDiffAt.of_succ
deleted theorem ContMDiffAt.prod_map'
deleted theorem ContMDiffAt.prod_map
deleted theorem ContMDiffAt.smoothAt
deleted theorem ContMDiffAt.snd
deleted def ContMDiffAt
deleted theorem ContMDiffOn.clm_apply
deleted theorem ContMDiffOn.clm_comp
deleted theorem ContMDiffOn.clm_precomp
deleted theorem ContMDiffOn.clm_prodMap
deleted theorem ContMDiffOn.comp'
deleted theorem ContMDiffOn.comp
deleted theorem ContMDiffOn.congr
deleted theorem ContMDiffOn.contMDiffAt
deleted theorem ContMDiffOn.continuousOn
deleted theorem ContMDiffOn.mono
deleted theorem ContMDiffOn.of_le
deleted theorem ContMDiffOn.of_succ
deleted theorem ContMDiffOn.prod_map
deleted theorem ContMDiffOn.prod_mk
deleted theorem ContMDiffOn.prod_mk_space
deleted theorem ContMDiffOn.smoothOn
deleted theorem ContMDiffOn.smul
deleted def ContMDiffOn
deleted theorem ContMDiffWithinAt.comp'
deleted theorem ContMDiffWithinAt.comp
deleted theorem ContMDiffWithinAt.congr
deleted theorem ContMDiffWithinAt.fst
deleted theorem ContMDiffWithinAt.insert
deleted theorem ContMDiffWithinAt.mono
deleted theorem ContMDiffWithinAt.of_le
deleted theorem ContMDiffWithinAt.of_succ
deleted theorem ContMDiffWithinAt.prod_mk
deleted theorem ContMDiffWithinAt.smul
deleted theorem ContMDiffWithinAt.snd
deleted def ContMDiffWithinAt
deleted theorem Smooth.comp_smoothOn
deleted theorem Smooth.contMDiff
deleted theorem Smooth.fst
deleted theorem Smooth.smoothAt
deleted theorem Smooth.smoothOn
deleted theorem Smooth.snd
deleted def Smooth
deleted theorem SmoothAt.contMDiffAt
deleted theorem SmoothAt.fst
deleted theorem SmoothAt.smoothWithinAt
deleted theorem SmoothAt.snd
deleted def SmoothAt
deleted theorem SmoothOn.comp_smooth
deleted theorem SmoothOn.contMDiffOn
deleted theorem SmoothOn.smoothAt
deleted def SmoothOn
deleted theorem SmoothWithinAt.smoothAt
deleted def SmoothWithinAt
deleted theorem contDiffWithinAtProp_id
deleted theorem contDiffWithinAtProp_self
deleted theorem contMDiffAt_const
deleted theorem contMDiffAt_extChartAt'
deleted theorem contMDiffAt_extChartAt
deleted theorem contMDiffAt_extend
deleted theorem contMDiffAt_fst
deleted theorem contMDiffAt_id
deleted theorem contMDiffAt_iff
deleted theorem contMDiffAt_iff_target
deleted theorem contMDiffAt_one
deleted theorem contMDiffAt_pi_space
deleted theorem contMDiffAt_prod_iff
deleted theorem contMDiffAt_snd
deleted theorem contMDiffAt_top
deleted theorem contMDiffOn_chart
deleted theorem contMDiffOn_chart_symm
deleted theorem contMDiffOn_congr
deleted theorem contMDiffOn_const
deleted theorem contMDiffOn_extChartAt
deleted theorem contMDiffOn_extend_symm
deleted theorem contMDiffOn_fst
deleted theorem contMDiffOn_id
deleted theorem contMDiffOn_iff
deleted theorem contMDiffOn_iff_target
deleted theorem contMDiffOn_model_symm
deleted theorem contMDiffOn_one
deleted theorem contMDiffOn_pi_space
deleted theorem contMDiffOn_snd
deleted theorem contMDiffOn_top
deleted theorem contMDiffOn_univ
deleted theorem contMDiffWithinAt_congr
deleted theorem contMDiffWithinAt_const
deleted theorem contMDiffWithinAt_fst
deleted theorem contMDiffWithinAt_id
deleted theorem contMDiffWithinAt_iff'
deleted theorem contMDiffWithinAt_iff
deleted theorem contMDiffWithinAt_iff_nat
deleted theorem contMDiffWithinAt_inter'
deleted theorem contMDiffWithinAt_inter
deleted theorem contMDiffWithinAt_one
deleted theorem contMDiffWithinAt_snd
deleted theorem contMDiffWithinAt_top
deleted theorem contMDiffWithinAt_univ
deleted theorem contMDiff_const
deleted theorem contMDiff_fst
deleted theorem contMDiff_id
deleted theorem contMDiff_iff
deleted theorem contMDiff_iff_contDiff
deleted theorem contMDiff_iff_target
deleted theorem contMDiff_inclusion
deleted theorem contMDiff_model
deleted theorem contMDiff_of_support
deleted theorem contMDiff_one
deleted theorem contMDiff_pi_space
deleted theorem contMDiff_prod_iff
deleted theorem contMDiff_snd
deleted theorem contMDiff_top
deleted theorem smoothAt_const
deleted theorem smoothAt_fst
deleted theorem smoothAt_id
deleted theorem smoothAt_iff_target
deleted theorem smoothAt_one
deleted theorem smoothAt_pi_space
deleted theorem smoothAt_prod_iff
deleted theorem smoothAt_snd
deleted theorem smoothOn_const
deleted theorem smoothOn_fst
deleted theorem smoothOn_id
deleted theorem smoothOn_iff
deleted theorem smoothOn_iff_target
deleted theorem smoothOn_one
deleted theorem smoothOn_pi_space
deleted theorem smoothOn_snd
deleted theorem smoothOn_univ
deleted theorem smoothWithinAt_const
deleted theorem smoothWithinAt_fst
deleted theorem smoothWithinAt_id
deleted theorem smoothWithinAt_iff
deleted theorem smoothWithinAt_iff_target
deleted theorem smoothWithinAt_one
deleted theorem smoothWithinAt_pi_space
deleted theorem smoothWithinAt_snd
deleted theorem smoothWithinAt_univ
deleted theorem smooth_const
deleted theorem smooth_fst
deleted theorem smooth_id
deleted theorem smooth_iff
deleted theorem smooth_iff_target
deleted theorem smooth_inclusion
deleted theorem smooth_one
deleted theorem smooth_pi_space
deleted theorem smooth_prod_assoc
deleted theorem smooth_prod_iff
deleted theorem smooth_smul
deleted theorem smooth_snd
added theorem contMDiffAt_extChartAt
added theorem contMDiffAt_extend
added theorem contMDiffOn_chart
added theorem contMDiffOn_chart_symm
added theorem contMDiffOn_extChartAt
added theorem contMDiffOn_model_symm
added theorem contMDiff_model
added theorem ContMDiff.comp
added theorem ContMDiffAt.comp_of_eq
added theorem ContMDiffOn.comp'
added theorem ContMDiffOn.comp
added theorem ContMDiffWithinAt.comp
added theorem Smooth.comp_smoothOn
added theorem SmoothOn.comp_smooth
added theorem contMDiffAt_const
added theorem contMDiffAt_id
added theorem contMDiffAt_one
added theorem contMDiffOn_const
added theorem contMDiffOn_id
added theorem contMDiffOn_one
added theorem contMDiffWithinAt_id
added theorem contMDiffWithinAt_one
added theorem contMDiff_const
added theorem contMDiff_id
added theorem contMDiff_inclusion
added theorem contMDiff_of_support
added theorem contMDiff_one
added theorem smoothAt_const
added theorem smoothAt_id
added theorem smoothAt_one
added theorem smoothOn_const
added theorem smoothOn_id
added theorem smoothOn_one
added theorem smoothWithinAt_const
added theorem smoothWithinAt_id
added theorem smoothWithinAt_one
added theorem smooth_const
added theorem smooth_id
added theorem smooth_inclusion
added theorem smooth_one
added theorem ContMDiff.contMDiffAt
added theorem ContMDiff.contMDiffOn
added theorem ContMDiff.continuous
added theorem ContMDiff.of_le
added theorem ContMDiff.of_succ
added theorem ContMDiff.smooth
added def ContMDiff
added theorem ContMDiffAt.of_le
added theorem ContMDiffAt.of_succ
added theorem ContMDiffAt.smoothAt
added def ContMDiffAt
added theorem ContMDiffOn.congr
added theorem ContMDiffOn.mono
added theorem ContMDiffOn.of_le
added theorem ContMDiffOn.of_succ
added theorem ContMDiffOn.smoothOn
added def ContMDiffOn
added theorem ContMDiffWithinAt.mono
added theorem Smooth.contMDiff
added theorem Smooth.smoothAt
added theorem Smooth.smoothOn
added def Smooth
added theorem SmoothAt.contMDiffAt
added def SmoothAt
added theorem SmoothOn.contMDiffOn
added theorem SmoothOn.smoothAt
added def SmoothOn
added def SmoothWithinAt
added theorem contMDiffAt_iff
added theorem contMDiffAt_iff_target
added theorem contMDiffAt_top
added theorem contMDiffOn_congr
added theorem contMDiffOn_iff
added theorem contMDiffOn_iff_target
added theorem contMDiffOn_top
added theorem contMDiffOn_univ
added theorem contMDiffWithinAt_iff'
added theorem contMDiffWithinAt_iff
added theorem contMDiffWithinAt_top
added theorem contMDiffWithinAt_univ
added theorem contMDiff_iff
added theorem contMDiff_iff_target
added theorem contMDiff_top
added theorem smoothAt_iff_target
added theorem smoothOn_iff
added theorem smoothOn_iff_target
added theorem smoothOn_univ
added theorem smoothWithinAt_iff
added theorem smoothWithinAt_univ
added theorem smooth_iff
added theorem smooth_iff_target
added theorem ContMDiff.clm_apply
added theorem ContMDiff.clm_comp
added theorem ContMDiff.clm_postcomp
added theorem ContMDiff.clm_precomp
added theorem ContMDiff.clm_prodMap
added theorem ContMDiff.smul
added theorem ContMDiffAt.clm_comp
added theorem ContMDiffOn.clm_apply
added theorem ContMDiffOn.clm_comp
added theorem ContMDiffOn.smul
added theorem ContMDiffWithinAt.smul
added theorem contMDiff_iff_contDiff
added theorem smooth_smul
added theorem ContMDiff.fst
added theorem ContMDiff.prod_map
added theorem ContMDiff.snd
added theorem ContMDiffAt.fst
added theorem ContMDiffAt.prod_map'
added theorem ContMDiffAt.prod_map
added theorem ContMDiffAt.snd
added theorem ContMDiffOn.prod_map
added theorem ContMDiffOn.prod_mk
added theorem ContMDiffWithinAt.fst
added theorem ContMDiffWithinAt.snd
added theorem Smooth.fst
added theorem Smooth.snd
added theorem SmoothAt.fst
added theorem SmoothAt.snd
added theorem contMDiffAt_fst
added theorem contMDiffAt_pi_space
added theorem contMDiffAt_prod_iff
added theorem contMDiffAt_snd
added theorem contMDiffOn_fst
added theorem contMDiffOn_pi_space
added theorem contMDiffOn_snd
added theorem contMDiffWithinAt_fst
added theorem contMDiffWithinAt_snd
added theorem contMDiff_fst
added theorem contMDiff_pi_space
added theorem contMDiff_prod_iff
added theorem contMDiff_snd
added theorem smoothAt_fst
added theorem smoothAt_pi_space
added theorem smoothAt_prod_iff
added theorem smoothAt_snd
added theorem smoothOn_fst
added theorem smoothOn_pi_space
added theorem smoothOn_snd
added theorem smoothWithinAt_fst
added theorem smoothWithinAt_snd
added theorem smooth_fst
added theorem smooth_pi_space
added theorem smooth_prod_assoc
added theorem smooth_prod_iff
added theorem smooth_snd