Commit 2026-01-30 15:11 409fcdc2

View on Github →

chore: golf using fun_prop (#34441) The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in #31607.

Estimated changes

modified theorem measurable_edist_left
modified theorem measurable_edist_right
modified theorem continuous_div_left'
modified theorem continuous_div_right'
modified theorem continuous_mul_left
modified theorem continuous_mul_right
modified theorem Metric.isClosed_closedBall
modified theorem Metric.isClosed_sphere
modified theorem continuous_projIcc