## Stream: condensed mathematics

### Topic: breen_deligne refactor

#### Johan Commelin (Apr 09 2021 at 20:03):

I'm refactoring a bunch of stuff in breen_deligne/* to make it easier to prove things about the homotopy.
Going to bed now. Pushed my wip to bd_refactor.
There were some sorries in those files (on master) but it probably doesn't make sense to work on those, until the refactor is done.

#### Johan Commelin (Apr 13 2021 at 15:05):

This refactor is now done, and merged into master.

#### Johan Commelin (Apr 13 2021 at 15:09):

At some point we'll need some constants c_ c' : nat -> nnreal that play well with breen_deligne.eg.
Here eg is the explicit example of breen_deligne.package, see breen_deligne/eg.lean.

What we need is that for variable r r' : nnreal (satisfying [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r' ≤ 1)]) we have

• eg.very_suitable r r' c_ (so c_ shall depend on r and r')
• eg.adept c_ c' (so c' shall be constructed in terms of a c_, here r and r' don't play a role)

#### Johan Commelin (Apr 13 2021 at 15:10):

So, if you like playing with division/inverses of non-negative reals, then feel free to add constructions of such sequences to eg.lean.

Last updated: May 09 2021 at 21:10 UTC