Theorem LightCondSet.hom_naturality_apply

Modification history

2024-08-30 08:52

Mathlib/Condensed/Light/Basic.lean

style: some formatting fixes (#16263) …

Modified LightCondSet.hom_naturality_apply View on Github →

2024-07-19 14:02

Mathlib/Condensed/Light/Basic.lean

feat(LightCondensed): the functor from `TopCat` to `LightCondSet` is a faithful right adjoint (#14506)

Added LightCondSet.hom_naturality_apply View on Github →