English
Let r be a relation α → β, s a relation β → γ, and l a filter on γ. The r-comap construction is associative with respect to composition: applying rcomap along r after applying rcomap along s to l yields the same as applying rcomap along the composed relation r ∘ s to l.
Русский
Пусть r — отношение α → β, s — отношение β → γ, и l — фильтр над γ. Операция rcomap совместима с композицией: rcomap r (rcomap s l) = rcomap (r ∘ s) l.
LaTeX
$$$ \\mathrm{rcomap}_{r}(\\mathrm{rcomap}_{s}(l)) = \\mathrm{rcomap}_{r\\circ s}(l) $$$
Lean4
theorem rcomap_rcomap (r : SetRel α β) (s : SetRel β γ) (l : Filter γ) : rcomap r (rcomap s l) = rcomap (r.comp s) l :=
filter_eq <| by
ext t
simp only [rcomap_sets, SetRel.image, Filter.mem_sets, Set.mem_setOf_eq, SetRel.core_comp]
constructor
· rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
exact ⟨v, vsets, Set.Subset.trans (SetRel.core_mono hv) h⟩
rintro ⟨t, tsets, ht⟩
exact ⟨SetRel.core s t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩
