Theorem LightCondMod.isDiscrete_iff_isDiscrete_forget

Modification history

2024-10-17 08:31
Mathlib/Condensed/Discrete/Characterization.lean
feat(Condensed): characterisation of discrete (light) condensed sets and modules (#14027) …
Added LightCondMod.isDiscrete_iff_isDiscrete_forgetView on Github →