Theorem LightCondensed.equalizerCondition

Modification history

2026-03-06 08:34

Mathlib/Condensed/Light/Explicit.lean

refactor(CategoryTheory/Sites): redefine the category of sheaves using `ObjectProperty.FullSubcategory` (#36081) …

Modified LightCondensed.equalizerCondition View on Github →

2024-06-07 09:26

Mathlib/Condensed/Light/Explicit.lean

feat(Condensed): explicit sheaf condition for light condensed sets (#13503) …

Added LightCondensed.equalizerCondition View on Github →