Commit 2024-01-12 09:21 52bef362

View on Github →

chore(Topology/PartialHomeomorph): re-use one variable (#9630) General housekeeping; this also makes re-naming the types to Greek letters easier.

Estimated changes

Modified Mathlib/Topology/PartialHomeomorph.lean

modified theorem PartialHomeomorph.eventually_left_inverse'

modified theorem PartialHomeomorph.eventually_left_inverse

modified theorem PartialHomeomorph.eventually_ne_nhdsWithin

modified theorem PartialHomeomorph.eventually_nhds'

modified theorem PartialHomeomorph.eventually_nhds

modified theorem PartialHomeomorph.eventually_nhdsWithin'

modified theorem PartialHomeomorph.eventually_nhdsWithin

modified theorem PartialHomeomorph.eventually_right_inverse'

modified theorem PartialHomeomorph.eventually_right_inverse

modified theorem PartialHomeomorph.image_source_eq_target

modified theorem PartialHomeomorph.map_nhdsWithin_eq

modified theorem PartialHomeomorph.map_nhdsWithin_preimage_eq

modified theorem PartialHomeomorph.replaceEquiv_eq_self

modified theorem PartialHomeomorph.secondCountableTopology_source

modified theorem PartialHomeomorph.symm_image_target_eq_source