rcomap_compose — Mathlib

English

The r-comap operator respects composition: composing two r-comaps is the same as taking the r-comap along the composite relation. In symbols, rcomap r ∘ rcomap s = rcomap (r ∘ s).

Русский

Оператор rcomap сохраняет композицию: rcomap r ∘ rcomap s = rcomap (r ∘ s).

LaTeX

$$$ (\\mathrm{rcomap}\\, r) \\circ (\\mathrm{rcomap}\\, s) = \\mathrm{rcomap}\\, (r \\circ s) $$$

Lean4

@[simp]
theorem rcomap_compose (r : SetRel α β) (s : SetRel β γ) : rcomap r ∘ rcomap s = rcomap (r.comp s) :=
  funext <| rcomap_rcomap _ _

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