Theorem Condensed.equalizerCondition

Modification history

2026-03-06 08:34

Mathlib/Condensed/Explicit.lean

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

Modified Condensed.equalizerCondition View on Github →

2024-05-23 09:04

Mathlib/Condensed/Explicit.lean

feat(Condensed): prove the explicit sheaf condition for a general target category (#12870) …

Added Condensed.equalizerCondition View on Github →