English
For a condensed object X in A, the presheaf is a sheaf on Stonean with respect to the coherent topology: the transported object along StoneanToCompHaus is a sheaf.
Русский
Для конденсированного объекта X в A предшествующая функция является sheaf на Stonean при когерентной топологии: перенос через StoneanToCompHaus образует sheaf.
LaTeX
$$$$\mathrm{Presheaf.IsSheaf}(\mathrm{coherentTopology\;Stonean})(\mathrm{StoneanToCompHaus}^{\mathrm{op}} \circ X).$$$$
Lean4
theorem isSheafStonean [∀ Y, HasLimitsOfShape (StructuredArrow Y Stonean.toCompHaus.{u}.op) A] :
Presheaf.IsSheaf (coherentTopology Stonean) (Stonean.toCompHaus.op ⋙ X.val) :=
((StoneanCompHaus.equivalence A).inverse.obj X).cond
