instCoeFunForallSetPresieve — Mathlib

English

There is a canonical coercion from the category of Pretopologies on C to the function space assigning to each object X of C the set of presieves on X; equivalently, each Pretopology J on C determines, for every X, a collection J X of coverings, viewed as a subset of Presieve X.

Русский

Существует каноническое отображение из множества препотопологий на C в функциям, сопоставляющим каждому объекту X множество покрытий на X; иначе говоря, любая препотопология J на C определяет, для каждого X, множество покрытий J X, как подмножество Presieve X.

LaTeX

$$$\\text{There is a canonical coercion } \\mathrm{coe}: \\mathrm{Pretopology}(C) \\to \\prod_{X\\in \\mathrm{Obj}(C)} \\mathcal{P}(\\mathrm{Presieve}(X)) \\text{ defined by } (\\mathrm{coe}(J))(X) = J.X,$$$

Lean4

instance : CoeFun (Pretopology C) fun _ => ∀ X : C, Set (Presieve X) :=
  ⟨fun J ↦ J.coverings⟩

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