Theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart'

Modification history

2026-06-11 13:02

Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

feat: drop `HasGroupoid` assumption in several `LiftPropAt` lemmas (#40475)

Modified StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart'View on Github →

2023-04-17 07:01

Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

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

Added StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart'View on Github →