sheafify_sheafify — Mathlib

English

Applying sheafification twice is the same as applying it once: (G.sheafify J).sheafify J = G.sheafify J.

Русский

Применение шейфайфикации дважды равно одному разу: (G.sheafify J).sheafify J = G.sheafify J.

LaTeX

$$$ (G.sheafify J).sheafify J = G.sheafify J $$$

Lean4

theorem sheafify_sheafify (h : Presieve.IsSheaf J F) : (G.sheafify J).sheafify J = G.sheafify J :=
  ((Subpresheaf.eq_sheafify_iff _ h).mpr <| G.sheafify_isSheaf h).symm

Похожие утверждения