English
One direction of taking inverse map of a filter under a relation: rcomap (a relation) f yields a filter on α consisting of sets generated by a certain relation-image construction.
Русский
Обратное отображение фильтра по отношению: rcomap(r,f) образует фильтр на α, порождаемый соответствующей конструкцией изображения по отношению.
LaTeX
$$$\mathrm{rcomap}(r,f) = \{ \text{sets} := \mathrm{SetRel.image}\{(s,t) \mid r.core(s) \subseteq t\} f.sets, \dots \}$$$
Lean4
/-- One way of taking the inverse map of a filter under a relation. One generalization of
`Filter.comap` to relations. Note that `Rel.core` generalizes `Set.preimage`. -/
def rcomap (r : SetRel α β) (f : Filter β) : Filter α
where
sets := SetRel.image {(s, t) : _ × _ | r.core 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.core_inter a' b').subset.trans (Set.inter_subset_inter ha₂ hb₂)⟩
