Commit 2023-06-22 23:07 d6d8643f

View on Github →

chore: forward port leanprover-community/mathlib#19146 (#5371)

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added theorem TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

added theorem StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion

added theorem StructureGroupoid.LocalInvariantProp.liftProp_inclusion

Modified Mathlib/Topology/LocalHomeomorph.lean

added theorem LocalHomeomorph.map_subtype_source

added theorem LocalHomeomorph.subtypeRestr_symm_eqOn_of_le