PR #17081: feat(analysis/convex/continuous): Convex funct...

Stream: triage

[Random Issue Bot]

Today I chose PR 17081 for discussion!

feat(analysis/convex/continuous): Convex functions are continuous
Created by @Yaël Dillies (@YaelDillies) on 2022-10-20
Labels: help wanted, WIP, t-analysis

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

Waiting on @Paul A. Reichert's work! How is it going?

[Paul A. Reichert]

I'm working on it, never forgot it -- the PR you looked over recently is a still part of the project. I proved the result about the intrinsic interior in a single file with some hundreds of lines and it takes me much longer than I expected to PR them in sufficiently small pieces. My three open PRs are the last ones that I have to integrate into mathlib before I can finally PR the intrinsic interior.

[Yaël Dillies]

Very nice! Do you need any help with splitting things up?