pullback_stable — Mathlib

English

If S is a covering sieve on X and f: Y → X is any morphism, then the pullback sieve S.pullback f is covering on Y.

Русский

Если S покрывающий на X и f: Y → X произвольна, то вытяжка S.pullback f покрывает Y.

LaTeX

$$S ∈ J X → S.pullback f ∈ J Y$$

Lean4

/-- Also known as the stability axiom. -/
@[simp]
theorem pullback_stable (f : Y ⟶ X) (hS : S ∈ J X) : S.pullback f ∈ J Y :=
  J.pullback_stable' f hS

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