rel_bind — Mathlib

English

If a Relator lifts a relation r to multisets via Relator.LiftFun, then bind respects this relation: Rel p (s.bind f) (t.bind g).

Русский

Если релятор поднимает отношение r до мультимножества посредством Relator.LiftFun, то связывание сохраняет это отношение: Rel p (s.bind f) (t.bind g).

LaTeX

$$$Rel\\ p\\ (s.bind f)\\ (t.bind g)$$$

Lean4

theorem rel_bind {r : α → β → Prop} {p : γ → δ → Prop} {s t} {f : α → Multiset γ} {g : β → Multiset δ}
    (h : (r ⇒ Rel p) f g) (hst : Rel r s t) : Rel p (s.bind f) (t.bind g) :=
  by
  apply rel_join
  rw [rel_map]
  exact hst.mono fun a _ b _ hr => h hr

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