transitive — Mathlib

English

If S is covering at X, and R is any sieve on X, and for every Y and f: Y → X, S f implies that the pullback of R along f is covering on Y, then R is covering on X.

Русский

Если S покрывает X, и R — любая решётка на X, и для каждого Y и f: Y → X, если S f, то вытяжка R вдоль f покрывает Y, то R покрывает X.

LaTeX

$$S ∈ J X → (∀ R, (∀ Y f, S f → R.pullback f ∈ J Y)) → R ∈ J X$$

Lean4

theorem transitive (hS : S ∈ J X) (R : Sieve X) (h : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f → R.pullback f ∈ J Y) : R ∈ J X :=
  J.transitive' hS R h

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