Commit 2026-05-14 02:11 fd1f5397
View on Github →chore: add SeparationQuotient.continuous_lift and mark as fun_prop (#39343)
Rename the existing SeparationQuotient.continuous_lift (which is an iff) to continuous_lift_iff, and add an alias for the converse direction. Use this to golf a proof using fun_prop.
Extracted from #39337.