Zulip Chat Archive
Stream: condensed mathematics
Topic: admissible
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.
Riccardo Brasca (Jan 26 2021 at 15:42):
I can do it. Ifleanproject build succeeds it's done, right?
Johan Commelin (Jan 26 2021 at 15:43):
please do it for double complexes as well
Riccardo Brasca (Jan 26 2021 at 15:44):
OK
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: Dec 20 2023 at 11:08 UTC