bind_covering — Mathlib

English

If S is a sieve on X and R assigns to each f: Y → X a sieve on Y, and S is covering, and R(H) is covering for each H arising from S f, then Sieve.bind S R is covering on X.

Русский

Если S — решёт на X, R задаёт для каждого f: Y → X решёт на Y, и S покрывает, а для каждого f соответствующее R(H) покрывает, тогда Sieve.bind S R покрывает X.

LaTeX

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

Lean4

theorem bind_covering {S : Sieve X} {R : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → Sieve Y} (hS : S ∈ J X)
    (hR : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (H : S f), R H ∈ J Y) : Sieve.bind S R ∈ J X :=
  J.transitive hS _ fun _ f hf => superset_covering J (Sieve.le_pullback_bind S R f hf) (hR hf)

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