covers_iff_mem_of_isClosed — Mathlib

English

If S is J₁-closed, then for any Y, f: Y ⟶ X, J₁.Covers S f holds iff S f holds.

Русский

Если S замкнута по J₁, то для любого f: Y ⟶ X верно J₁.Covers S f тогда и только тогда, когда S f действительно присутствует.

LaTeX

$$$h:\\; J_1.IsClosed S \\Rightarrow \\forall f:Y\\to X,\\; J_1.\\ Covers S f \\iff S f$$$

Lean4

/-- If `S` is `J₁`-closed, then `S` covers exactly the arrows it contains. -/
theorem covers_iff_mem_of_isClosed {X : C} {S : Sieve X} (h : J₁.IsClosed S) {Y : C} (f : Y ⟶ X) :
    J₁.Covers S f ↔ S f :=
  ⟨h _, J₁.arrow_max _ _⟩

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