rmap_rmap — Mathlib

English

RMap is associative with respect to composition of relations: rmap s (rmap r l) = rmap (r.comp s) l.

Русский

Сопоставление через отношение совместимо с композициями: rmap s (rmap r l) = rmap (r.comp s) l.

LaTeX

$$$\mathrm{rmap}(s) (\mathrm{rmap}(r) l) = \mathrm{rmap}(r \circ s) l$$$

Lean4

@[simp]
theorem rmap_rmap (r : SetRel α β) (s : SetRel β γ) (l : Filter α) : rmap s (rmap r l) = rmap (r.comp s) l :=
  filter_eq <| by simp [rmap_sets, Set.preimage, SetRel.core_comp]

Похожие утверждения