Theorem Condensed.isoFinYonedaComponents_inv_comp

Modification history

2024-11-02 17:02
Mathlib/Condensed/Discrete/Colimit.lean
chore: remove superfluous decidability assumptions (#18553) …
Modified Condensed.isoFinYonedaComponents_inv_compView on Github →
2024-10-16 04:43
Mathlib/Condensed/Discrete/Colimit.lean
feat(Condensed): colimit characterization of discrete condensed sets (#15566) …
Added Condensed.isoFinYonedaComponents_inv_compView on Github →