bind_congr — Mathlib

English

If s1 ~ʷ s2 and for all a, f1 a ~ʷ f2 a, then bind s1 f1 ~ʷ bind s2 f2.

Русский

Если s1 эквивалентны s2 и для каждого элемента a выполнено f1 a ~ʷ f2 a, то связывание s1 с f1 эквивалентно связыванию s2 с f2.

LaTeX

$$$ \forall {\alpha,\beta}, {s1 s2: \mathrm{WSeq}\,\alpha}, {f1 f2: \alpha \to \mathrm{WSeq}\,\beta},\; s1 \sim_W s2 \to (\forall a, f1 a \sim_W f2 a) \Rightarrow (s1.bind f1) \sim_W (s2.bind f2)$$$

Lean4

theorem bind_congr {s1 s2 : WSeq α} {f1 f2 : α → WSeq β} (h1 : s1 ~ʷ s2) (h2 : ∀ a, f1 a ~ʷ f2 a) :
    bind s1 f1 ~ʷ bind s2 f2 :=
  liftRel_bind _ _ h1 fun {a b} h => by rw [h]; apply h2

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