arrow_trans — Mathlib

English

If J.Covers S f and for all g with domain Y, whenever S g holds, J.Covers R g, then J.Covers R f.

Русский

Если J.Covers S f и для всех g, если S g, то J.Covers R g, тогда J.Covers R f.

LaTeX

$$J.Covers S f ∧ (∀ g, S g → J.Covers R g) ⇒ J.Covers R f$$

Lean4

/-- The transitivity axiom in 'arrow' form: If `S` covers `f` and every arrow in `S` is covered by
`R`, then `R` covers `f`.
-/
theorem arrow_trans (f : Y ⟶ X) (S R : Sieve X) (h : J.Covers S f) :
    (∀ {Z : C} (g : Z ⟶ X), S g → J.Covers R g) → J.Covers R f :=
  by
  intro k
  apply J.transitive h
  intro Z g hg
  rw [← Sieve.pullback_comp]
  apply k (g ≫ f) hg

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