isSeparated — Mathlib

English

The evaluation of yonedaULiftEquiv at a morphism f aligns with evaluation at identity: it returns f.val.app (op X) ⟨𝟙 X⟩.

Русский

Оценка yonedaULiftEquiv на морфизм f согласуется с оценкой по тождественному: возвращает f.val.app (op X) ⟨𝟙 X⟩.

LaTeX

$$$\text{yonedaULiftEquivApply}\ f = f.\val.app\ (op X) \ ⟨𝟙 X\rangle$$$

Lean4

/-- Every subpresheaf of a separated presheaf is itself separated. -/
theorem isSeparated {J : GrothendieckTopology C} (h : Presieve.IsSeparated J F) : Presieve.IsSeparated J G.toPresheaf :=
  fun _ S hS _ _ _ hx₁ hx₂ ↦ Subtype.ext <| h S hS _ _ _ (hx₁.map G.ι) (hx₂.map G.ι)

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