Commit 2025-10-28 09:17 e9633158

feat: further extensions of the differential geometry elaborators (#30413) Also infer the model with corners on

• a space of continuous linear equivalences
• a closed real interval (Set.Icc)
• the complex upper half plane And add elaborators for HasMFDeriv(Within)At analogous to the mfderiv(Within) ones. Further cases, as well as products, disjoint unions or open subsets, will be covered in future PRs.