English
Let α and β be types and r a relation on α and β. For any filter f on β, the α-sets of the r-comap of f are precisely the pairs of subsets described by the relation r, namely the image of f.sets under the relation (s, t) with r.core s ⊆ t. In other words, the sets of rcomap r f are exactly those subsets S ⊆ α for which there exists a subset T ⊆ β with T ∈ f.sets and r.core(S) ⊆ T.
Русский
Пусть α и β — множества, r — отношение между α и β. Для любого фильтра f на β множества α внутри r-комапа f совпадают с образами по отношению SetRel изображения {(s, t) | r.core s ⊆ t} от множества f.sets. Другими словами, множества rcomap r f равны те подмножества S ⊆ α, для которых существует T ⊆ β с T ∈ f.sets и r.core(S) ⊆ T.
LaTeX
$$$ (rcomap\\, r\\, f).sets = \\{ S \\subseteq \\alpha \\\\mid \\exists T \\subseteq \\beta, T \\in f.sets \\\\wedge r.core(S) \\subseteq T \\} $$$
Lean4
theorem rcomap_sets (r : SetRel α β) (f : Filter β) :
(rcomap r f).sets = SetRel.image {(s, t) : _ × _ | r.core s ⊆ t} f.sets :=
rfl
