rmap_compose

Mathlib.Order.Filter.Partial

URI: https://scilib.ai/kg/mathlib#Filter.rmap_compose

English

The forward map under relation composes nicely: rmap s ∘ rmap r = rmap (r.comp s).

Русский

Порядок применения rmap сохраняется: rmap s ∘ rmap r = rmap (r.comp s).

LaTeX

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

Lean4

@[simp]
theorem rmap_compose (r : SetRel α β) (s : SetRel β γ) : rmap s ∘ rmap r = rmap (r.comp s) :=
  funext <| rmap_rmap _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru