Commit 2024-01-08 13:15 9df25a94

View on Github →

chore: last LocalHomeomorph -> PartialHomeomorph renames (#9238) Follow-up to #8982; a few lemma names were still wrong.

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/Geometry/Manifold/MFDeriv.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

deleted def FiberwiseLinear.localHomeomorph

added def FiberwiseLinear.partialHomeomorph

deleted theorem FiberwiseLinear.source_trans_localHomeomorph

added theorem FiberwiseLinear.source_trans_partialHomeomorph

deleted theorem FiberwiseLinear.target_trans_localHomeomorph

added theorem FiberwiseLinear.target_trans_partialHomeomorph

deleted theorem FiberwiseLinear.trans_localHomeomorph_apply

added theorem FiberwiseLinear.trans_partialHomeomorph_apply

Modified Mathlib/Topology/PartialHomeomorph.lean

modified theorem PartialHomeomorph.subtypeRestr_def

deleted theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_coe

deleted theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_source

deleted theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_target

added theorem TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_coe

added theorem TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_source

added theorem TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_target