Commit 2024-07-22 08:59 fa5f4dce

View on Github →

feat(LightCondensed): the fully faithful embedding of sequential spaces in light condensed sets (#14618)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Condensed/Light/TopCatAdjunction.lean

added theorem LightCondSet.continuous_coinducingCoprod

added def LightCondSet.lightCondSetToSequential

added def LightCondSet.sequentialAdjunctionHomeo

Modified Mathlib/Condensed/Light/TopComparison.lean

Created Mathlib/Topology/Category/Sequential.lean

added def Sequential.fullyFaithfulSequentialToTop

added def Sequential.homeoOfIso

added def Sequential.isoEquivHomeo

added def Sequential.isoOfHomeo

added def Sequential.of

added def Sequential.sequentialToTop

added structure Sequential