Theorem LightCondSet.isDiscrete_tfae

Modification history

2025-03-13 02:38
Mathlib/Condensed/Discrete/Characterization.lean
chore: whitespace again (#22878) …
Modified LightCondSet.isDiscrete_tfaeView on Github →
2024-10-17 08:31
Mathlib/Condensed/Discrete/Characterization.lean
feat(Condensed): characterisation of discrete (light) condensed sets and modules (#14027) …
Added LightCondSet.isDiscrete_tfaeView on Github →