# Zulip Chat Archive

## 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