Commit 2024-01-05 10:45 a5346b6b

View on Github →

chore: rename in PartialEquiv, Homeomorph, PartialHomeomorph (#9430) Items 4-5 in reference Zulip Also added symm and trans definitions for PartialEquiv, Homeomorph, and PartialHomeomorph.

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

added theorem PartialEquiv.self_trans_symm

added theorem PartialEquiv.symm_trans_self

deleted theorem PartialEquiv.trans_self_symm

deleted theorem PartialEquiv.trans_symm_self

Modified Mathlib/Topology/Homeomorph.lean

Modified Mathlib/Topology/PartialHomeomorph.lean

added theorem PartialHomeomorph.self_trans_symm

added theorem PartialHomeomorph.symm_trans_self

deleted theorem PartialHomeomorph.trans_self_symm

deleted theorem PartialHomeomorph.trans_symm_self