overEquiv_le_overEquiv_iff — Mathlib

English

For sieves R1, R2 on Y, R1.overEquiv Y ≤ R2.overEquiv Y iff R1 ≤ R2.

Русский

Для севеев R1, R2 на Y верно: R1.overEquiv Y ≤ R2.overEquiv Y и только если R1 ≤ R2.

LaTeX

$$R1.overEquiv Y ≤ R2.overEquiv Y ↔ R1 ≤ R2$$

Lean4

theorem overEquiv_le_overEquiv_iff {X : C} {Y : Over X} (R₁ R₂ : Sieve Y) : R₁.overEquiv Y ≤ R₂.overEquiv Y ↔ R₁ ≤ R₂ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ Sieve.functorPushforward_monotone _ _ h⟩
  replace h : (overEquiv Y).symm (R₁.overEquiv Y) ≤ (overEquiv Y).symm (R₂.overEquiv Y) :=
    Sieve.functorPullback_monotone _ _ h
  simpa using h

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