Commit 2024-01-17 18:25 1dfae4b2

View on Github →

chore(Topology/Inseparable): re-use some variables (#9808)

Estimated changes

Modified Mathlib/Topology/Inseparable.lean

modified theorem SeparationQuotient.continuousAt_lift

modified theorem SeparationQuotient.continuousOn_lift

modified theorem SeparationQuotient.continuousWithinAt_lift

modified theorem SeparationQuotient.continuous_lift

modified theorem SeparationQuotient.tendsto_lift_nhdsWithin_mk

modified theorem SeparationQuotient.tendsto_lift_nhds_mk