Commit 2023-06-24 01:01 f87a803f

View on Github →

feat: port Geometry.Manifold.ContMdiff (#4656)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/ContMDiff.lean

added theorem ContDiff.comp_contMDiff

added theorem ContDiffAt.comp_contMDiffAt

added theorem ContDiffWithinAt.comp_contMDiffWithinAt

added def ContDiffWithinAtProp

added theorem ContMDiff.clm_apply

added theorem ContMDiff.clm_comp

added theorem ContMDiff.clm_prodMap

added theorem ContMDiff.comp

added theorem ContMDiff.comp_contMDiffOn

added theorem ContMDiff.contMDiffAt

added theorem ContMDiff.contMDiffOn

added theorem ContMDiff.continuous

added theorem ContMDiff.fst

added theorem ContMDiff.of_le

added theorem ContMDiff.of_succ

added theorem ContMDiff.prod_map

added theorem ContMDiff.prod_mk_space

added theorem ContMDiff.smooth

added theorem ContMDiff.smul

added theorem ContMDiff.snd

added def ContMDiff

added theorem ContMDiffAt.clm_apply

added theorem ContMDiffAt.clm_comp

added theorem ContMDiffAt.clm_prodMap

added theorem ContMDiffAt.comp_contMDiffWithinAt

added theorem ContMDiffAt.comp_of_eq

added theorem ContMDiffAt.congr_of_eventuallyEq

added theorem ContMDiffAt.contMDiffWithinAt

added theorem ContMDiffAt.continuousAt

added theorem ContMDiffAt.fst

added theorem ContMDiffAt.of_le

added theorem ContMDiffAt.of_succ

added theorem ContMDiffAt.prod_map'

added theorem ContMDiffAt.prod_map

added theorem ContMDiffAt.smoothAt

added theorem ContMDiffAt.snd

added def ContMDiffAt

added theorem ContMDiffOn.clm_apply

added theorem ContMDiffOn.clm_comp

added theorem ContMDiffOn.clm_prodMap

added theorem ContMDiffOn.comp'

added theorem ContMDiffOn.comp

added theorem ContMDiffOn.comp_contMDiff

added theorem ContMDiffOn.congr

added theorem ContMDiffOn.contMDiffAt

added theorem ContMDiffOn.continuousOn

added theorem ContMDiffOn.mono

added theorem ContMDiffOn.of_le

added theorem ContMDiffOn.of_succ

added theorem ContMDiffOn.prod_map

added theorem ContMDiffOn.prod_mk

added theorem ContMDiffOn.prod_mk_space

added theorem ContMDiffOn.smoothOn

added theorem ContMDiffOn.smul

added def ContMDiffOn

added theorem ContMDiffWithinAt.clm_apply

added theorem ContMDiffWithinAt.clm_comp

added theorem ContMDiffWithinAt.clm_prodMap

added theorem ContMDiffWithinAt.comp'

added theorem ContMDiffWithinAt.comp

added theorem ContMDiffWithinAt.comp_of_eq

added theorem ContMDiffWithinAt.congr

added theorem ContMDiffWithinAt.congr_of_eventuallyEq

added theorem ContMDiffWithinAt.contMDiffAt

added theorem ContMDiffWithinAt.continuousWithinAt

added theorem ContMDiffWithinAt.fst

added theorem ContMDiffWithinAt.mono

added theorem ContMDiffWithinAt.mono_of_mem

added theorem ContMDiffWithinAt.of_le

added theorem ContMDiffWithinAt.of_succ

added theorem ContMDiffWithinAt.prod_map'

added theorem ContMDiffWithinAt.prod_map

added theorem ContMDiffWithinAt.prod_mk

added theorem ContMDiffWithinAt.prod_mk_space

added theorem ContMDiffWithinAt.smoothWithinAt

added theorem ContMDiffWithinAt.smul

added theorem ContMDiffWithinAt.snd

added def ContMDiffWithinAt

added theorem ContinuousLinearMap.contMDiff

added theorem Filter.EventuallyEq.contMDiffAt_iff

added theorem Filter.EventuallyEq.contMDiffWithinAt_iff

added theorem Smooth.comp_smoothOn

added theorem Smooth.contMDiff

added theorem Smooth.fst

added theorem Smooth.smoothAt

added theorem Smooth.smoothOn

added theorem Smooth.snd

added def Smooth

added theorem SmoothAt.comp_smoothWithinAt

added theorem SmoothAt.contMDiffAt

added theorem SmoothAt.fst

added theorem SmoothAt.smoothWithinAt

added theorem SmoothAt.snd

added def SmoothAt

added theorem SmoothOn.comp_smooth

added theorem SmoothOn.contMDiffOn

added theorem SmoothOn.smoothAt

added def SmoothOn

added theorem SmoothWithinAt.contMDiffWithinAt

added theorem SmoothWithinAt.smoothAt

added def SmoothWithinAt

added theorem contDiffWithinAtProp_id

added theorem contDiffWithinAtProp_mono_of_mem

added theorem contDiffWithinAtProp_self

added theorem contDiffWithinAtProp_self_source

added theorem contDiffWithinAtProp_self_target

added theorem contDiffWithinAt_localInvariantProp

added theorem contMDiffAt_const

added theorem contMDiffAt_extChartAt'

added theorem contMDiffAt_extChartAt

added theorem contMDiffAt_extend

added theorem contMDiffAt_fst

added theorem contMDiffAt_id

added theorem contMDiffAt_iff

added theorem contMDiffAt_iff_contDiffAt

added theorem contMDiffAt_iff_contMDiffAt_nhds

added theorem contMDiffAt_iff_contMDiffOn_nhds

added theorem contMDiffAt_iff_of_mem_source

added theorem contMDiffAt_iff_source_of_mem_source

added theorem contMDiffAt_iff_target

added theorem contMDiffAt_iff_target_of_mem_source

added theorem contMDiffAt_of_mem_maximalAtlas

added theorem contMDiffAt_one

added theorem contMDiffAt_pi_space

added theorem contMDiffAt_prod_iff

added theorem contMDiffAt_snd

added theorem contMDiffAt_symm_of_mem_maximalAtlas

added theorem contMDiffAt_top

added theorem contMDiffOn_chart

added theorem contMDiffOn_chart_symm

added theorem contMDiffOn_congr

added theorem contMDiffOn_const

added theorem contMDiffOn_extChartAt

added theorem contMDiffOn_extChartAt_symm

added theorem contMDiffOn_extend_symm

added theorem contMDiffOn_fst

added theorem contMDiffOn_id

added theorem contMDiffOn_iff

added theorem contMDiffOn_iff_contDiffOn

added theorem contMDiffOn_iff_of_mem_maximalAtlas'

added theorem contMDiffOn_iff_of_mem_maximalAtlas

added theorem contMDiffOn_iff_of_subset_source'

added theorem contMDiffOn_iff_of_subset_source

added theorem contMDiffOn_iff_source_of_mem_maximalAtlas

added theorem contMDiffOn_iff_target

added theorem contMDiffOn_model_symm

added theorem contMDiffOn_of_locally_contMDiffOn

added theorem contMDiffOn_of_mem_contDiffGroupoid

added theorem contMDiffOn_of_mem_maximalAtlas

added theorem contMDiffOn_one

added theorem contMDiffOn_pi_space

added theorem contMDiffOn_snd

added theorem contMDiffOn_symm_of_mem_maximalAtlas

added theorem contMDiffOn_top

added theorem contMDiffOn_univ

added theorem contMDiffWithinAt_congr

added theorem contMDiffWithinAt_congr_nhds

added theorem contMDiffWithinAt_const

added theorem contMDiffWithinAt_fst

added theorem contMDiffWithinAt_id

added theorem contMDiffWithinAt_iff'

added theorem contMDiffWithinAt_iff

added theorem contMDiffWithinAt_iff_contDiffWithinAt

added theorem contMDiffWithinAt_iff_contMDiffOn_nhds

added theorem contMDiffWithinAt_iff_image

added theorem contMDiffWithinAt_iff_nat

added theorem contMDiffWithinAt_iff_of_mem_maximalAtlas

added theorem contMDiffWithinAt_iff_of_mem_source'

added theorem contMDiffWithinAt_iff_of_mem_source

added theorem contMDiffWithinAt_iff_source_of_mem_maximalAtlas

added theorem contMDiffWithinAt_iff_source_of_mem_source

added theorem contMDiffWithinAt_iff_target

added theorem contMDiffWithinAt_iff_target_of_mem_source

added theorem contMDiffWithinAt_insert_self

added theorem contMDiffWithinAt_inter'

added theorem contMDiffWithinAt_inter

added theorem contMDiffWithinAt_one

added theorem contMDiffWithinAt_pi_space

added theorem contMDiffWithinAt_prod_iff

added theorem contMDiffWithinAt_snd

added theorem contMDiffWithinAt_top

added theorem contMDiffWithinAt_univ

added theorem contMDiff_const

added theorem contMDiff_fst

added theorem contMDiff_id

added theorem contMDiff_iff

added theorem contMDiff_iff_contDiff

added theorem contMDiff_iff_target

added theorem contMDiff_inclusion

added theorem contMDiff_model

added theorem contMDiff_of_locally_contMDiffOn

added theorem contMDiff_of_support

added theorem contMDiff_one

added theorem contMDiff_pi_space

added theorem contMDiff_prod_iff

added theorem contMDiff_snd

added theorem contMDiff_top

added theorem isLocalStructomorphOn_contDiffGroupoid_iff

added theorem isLocalStructomorphOn_contDiffGroupoid_iff_aux

added theorem smoothAt_const

added theorem smoothAt_fst

added theorem smoothAt_id

added theorem smoothAt_iff_target

added theorem smoothAt_one

added theorem smoothAt_pi_space

added theorem smoothAt_prod_iff

added theorem smoothAt_snd

added theorem smoothOn_const

added theorem smoothOn_fst

added theorem smoothOn_id

added theorem smoothOn_iff

added theorem smoothOn_iff_target

added theorem smoothOn_one

added theorem smoothOn_pi_space

added theorem smoothOn_snd

added theorem smoothOn_univ

added theorem smoothWithinAt_const

added theorem smoothWithinAt_fst

added theorem smoothWithinAt_id

added theorem smoothWithinAt_iff

added theorem smoothWithinAt_iff_target

added theorem smoothWithinAt_one

added theorem smoothWithinAt_pi_space

added theorem smoothWithinAt_snd

added theorem smoothWithinAt_univ

added theorem smooth_const

added theorem smooth_fst

added theorem smooth_id

added theorem smooth_iff

added theorem smooth_iff_target

added theorem smooth_inclusion

added theorem smooth_one

added theorem smooth_pi_space

added theorem smooth_prod_assoc

added theorem smooth_prod_iff

added theorem smooth_smul

added theorem smooth_snd