We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 5a54f93 commit ae8e527Copy full SHA for ae8e527
Mathlib/Condensed/Explicit.lean
@@ -18,7 +18,7 @@ We give the following three explicit descriptions of condensed objects:
18
* `Condensed.ofSheafProfinite`: A finite-product-preserving presheaf on `Profinite`, satisfying
19
`EqualizerCondition`.
20
21
-* `Condensed.ofSheafStonean`: A finite-product-preserving presheaf on `CompHaus`, satisfying
+* `Condensed.ofSheafCompHaus`: A finite-product-preserving presheaf on `CompHaus`, satisfying
22
23
24
The property `EqualizerCondition` is defined in `Mathlib/CategoryTheory/Sites/RegularSheaves.lean`
0 commit comments