Commit 2026-06-23 09:25 41520dac

feat: tag the pointwise Continuous/ContDiff/Measurable operation families with to_fun (#40872) Several fun_prop lemma families about pointwise operations existed only in eta-expanded form (Continuous (fun x => (f x)⁻¹)), so fun_prop could not close the corresponding point-free goal (Continuous f⁻¹). This PR restates those families point-free and tags them with @[to_fun (attr := …)], which regenerates the eta twin (fun_inv, fun_sub, fun_pow, …). Both forms then carry fun_prop, mirroring the existing Continuous.mul / ContinuousOn.mul setup, so fun_prop now matches goals in either shape (with one caveat, see below). Because of the name change of the eta version, many downstream invocations of these theorems have their name changed slightly (e.g., .inv becomes .fun_inv). In most cases this was a mechanical change; there were a few unusual edge cases, noted below and in the more detailed attached report. For further discussion, see this Zulip thread. Functionally, this PR is similar to #35306, but now implemented over many further fun_prop lemmas. This PR was prepared by an AI agent, guided by myself. In particular the summary text in this comment was initially generated by AI and then edited by myself.