mem_toGrothendieck_iff — Mathlib

English

For a precoverage J with pullbacks and base-change stability, a sieve S is in toGrothendieck J X iff S is in Saturate J X S.

Русский

При покрытии J с тянутьками (pullbacks) и стабильностью по базовым изменениям, клин S принадлежит toGrothendieck J X тогда и только тогда, когда S принадлежит Saturate J X S.

LaTeX

$$$$ S \in toGrothendieck J X \iff S \in J.toCoverage.Saturate X S $$$$

Lean4

theorem mem_toGrothendieck_iff {J : Precoverage C} [J.HasPullbacks] [J.IsStableUnderBaseChange] {X : C} {S : Sieve X} :
    S ∈ toGrothendieck J X ↔ J.toCoverage.Saturate X S :=
  .rfl

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