English
Rcomap' is associative with respect to the inner application: applying rcomap' r to (rcomap' s l) equals rcomap' (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
@[simp]
theorem rcomap'_rcomap' (r : SetRel α β) (s : SetRel β γ) (l : Filter γ) :
rcomap' r (rcomap' s l) = rcomap' (r.comp s) l :=
Filter.ext fun t => by
simp only [mem_rcomap', SetRel.preimage_comp]
constructor
· rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
exact ⟨v, vsets, (SetRel.preimage_mono hv).trans h⟩
rintro ⟨t, tsets, ht⟩
exact ⟨s.preimage t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩
