Commit 2023-04-17 07:01 0ec9f461

View on Github →

feat: port Geometry.Manifold.LocalInvariantProperties (#3401)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

added def ChartedSpace.LiftProp

added def ChartedSpace.LiftPropAt

added def ChartedSpace.LiftPropOn

added def ChartedSpace.LiftPropWithinAt

added theorem ChartedSpace.liftPropAt_iff

added theorem ChartedSpace.liftProp_iff

added theorem LocalHomeomorph.isLocalStructomorphWithinAt_iff'

added theorem LocalHomeomorph.isLocalStructomorphWithinAt_iff

added theorem LocalHomeomorph.isLocalStructomorphWithinAt_source_iff

added theorem StructureGroupoid.HasGroupoid.comp

added def StructureGroupoid.IsLocalStructomorphWithinAt

added theorem StructureGroupoid.LocalInvariantProp.congr'

added theorem StructureGroupoid.LocalInvariantProp.congr

added theorem StructureGroupoid.LocalInvariantProp.congr_iff

added theorem StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin

added theorem StructureGroupoid.LocalInvariantProp.congr_nhdsWithin'

added theorem StructureGroupoid.LocalInvariantProp.congr_nhdsWithin

added theorem StructureGroupoid.LocalInvariantProp.congr_set

added theorem StructureGroupoid.LocalInvariantProp.is_local_nhds

added theorem StructureGroupoid.LocalInvariantProp.left_invariance

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_chart

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_congr_of_eventuallyEq

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_of_liftPropWithinAt

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_groupoid

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_symm_of_mem_maximalAtlas

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_chart

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_congr

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_congr_iff

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_indep_chart

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_mono

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_liftProp

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_locally_liftPropOn

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas

added theorem StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart'

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source_aux

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux2

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter'

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono_of_mem

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt_of_mem_nhds

added theorem StructureGroupoid.LocalInvariantProp.liftProp_id

added theorem StructureGroupoid.LocalInvariantProp.liftProp_of_locally_liftPropOn

added theorem StructureGroupoid.LocalInvariantProp.right_invariance

added structure StructureGroupoid.LocalInvariantProp

added theorem StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp

added theorem StructureGroupoid.liftPropOn_univ

added theorem StructureGroupoid.liftPropWithinAt_self

added theorem StructureGroupoid.liftPropWithinAt_self_source

added theorem StructureGroupoid.liftPropWithinAt_self_target

added theorem StructureGroupoid.liftPropWithinAt_univ