Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-20 14:35
93521b73
View on Github →
feat: condensed sets are equivalent to sheaves on
Stonean
and
Profinite
(
#6810
)
depends on:
#6809
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Condensed/Equivalence.lean
added
def
Condensed.ProfiniteCompHaus.equivalence
added
theorem
Condensed.StoneanCompHaus.coherentTopology_is_induced
added
theorem
Condensed.StoneanCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
added
theorem
Condensed.StoneanCompHaus.coverDense
added
theorem
Condensed.StoneanCompHaus.coverLifting
added
theorem
Condensed.StoneanCompHaus.coverPreserving
added
def
Condensed.StoneanCompHaus.equivalence
added
theorem
Condensed.StoneanCompHaus.generate_singleton_mem_coherentTopology
added
theorem
Condensed.StoneanProfinite.coherentTopology_is_induced
added
theorem
Condensed.StoneanProfinite.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
added
theorem
Condensed.StoneanProfinite.coverDense
added
theorem
Condensed.StoneanProfinite.coverLifting
added
theorem
Condensed.StoneanProfinite.coverPreserving
added
def
Condensed.StoneanProfinite.equivalence
added
theorem
Condensed.StoneanProfinite.generate_singleton_mem_coherentTopology