English
The forward image of a filter under a relation is the filter on β whose sets are those whose r-core is in l.
Русский
Преобразование фильтра по отношению — это фильтр на β, множества которого состоят из таких подмножеств s, что r.core s ∈ l.
LaTeX
$$$(l \mathrm{.rmap}\ r).\mathrm{sets} = \{ s \subseteq \beta \mid r.\mathrm{core}(s) \in l \}$$$
Lean4
/-- The forward map of a filter under a relation. Generalization of `Filter.map` to relations. Note
that `Rel.core` generalizes `Set.preimage`. -/
def rmap (r : SetRel α β) (l : Filter α) : Filter β
where
sets := {s | r.core s ∈ l}
univ_sets := by simp
sets_of_superset hs st := mem_of_superset hs (SetRel.core_mono st)
inter_sets hs
ht := by
simp only [Set.mem_setOf_eq]
convert inter_mem hs ht
rw [← SetRel.core_inter]
