Theorem Condensed.StoneanCompHaus.generate_singleton_mem_coherentTopology

Modification history

2024-04-16 10:25

Mathlib/Condensed/Equivalence.lean

refactor(CategoryTheory): more general form of the characterisation of condensed sets as sheaves on `Stonean` (#11518) …

Deleted Condensed.StoneanCompHaus.generate_singleton_mem_coherentTopology View on Github →

2023-10-20 14:35

Mathlib/Condensed/Equivalence.lean

feat: condensed sets are equivalent to sheaves on `Stonean` and `Profinite` (#6810) …

Added Condensed.StoneanCompHaus.generate_singleton_mem_coherentTopology View on Github →