Zulip Chat Archive

Stream: condensed mathematics

Topic: admissible


view this post on Zulip Johan Commelin (Jan 26 2021 at 15:39):

We should change the definition of admissible from bound_by f 1 to \forall x, \|f x\| \le x. The latter inequality is what we want to use in practice.
If someone wants to refactor, please go ahead.

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 15:42):

I can do it. Ifleanproject build succeeds it's done, right?

view this post on Zulip Johan Commelin (Jan 26 2021 at 15:43):

please do it for double complexes as well

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 15:44):

OK

view this post on Zulip Riccardo Brasca (Jan 26 2021 at 16:10):

It's done... it was used only in the snake lemma, to that was really fast


Last updated: May 09 2021 at 22:13 UTC