English
A generalized inverse image of a filter along a relation. rcomap' is a definition generalizing rcomap, with sets defined by r.preimage s ⊆ t. It equips α with a filter whose sets are built by this relational image.
Русский
Обобщение обратного образа фильтра вдоль отношения: rcomap' — обобщение rcomap с множесвами, задаваемыми через r.preimage s ⊆ t.
LaTeX
$$$ (\\mathrm{rcomap}'\\, r\\, f).\\mathrm{sets} = \\operatorname{SetRel.image}\\{(s,t) \\mid r.preimage s \\subseteq t\\} f.sets $$$
Lean4
/-- One way of taking the inverse map of a filter under a relation. Generalization of `Filter.comap`
to relations. -/
def rcomap' (r : SetRel α β) (f : Filter β) : Filter α
where
sets := SetRel.image {(s, t) : _ × _ | r.preimage s ⊆ t} f.sets
univ_sets := ⟨Set.univ, univ_mem, Set.subset_univ _⟩
sets_of_superset := fun ⟨a', ha', ma'a⟩ ab => ⟨a', ha', ma'a.trans ab⟩
inter_sets := fun ⟨a', ha₁, ha₂⟩ ⟨b', hb₁, hb₂⟩ =>
⟨a' ∩ b', inter_mem ha₁ hb₁, r.preimage_inter_subset.trans (Set.inter_subset_inter ha₂ hb₂)⟩
