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, тогда bind s1 f1 ≈ bind s2 f2.

LaTeX

$$$\bigl(s_1 \sim s_2\bigr) \rightarrow \bigl(\forall a,\ f_1 a \sim f_2 a\bigr) \rightarrow \bigl(\mathrm{bind}\ s_1\ f_1 \sim \mathrm{bind}\ s_2\ f_2\bigr)$$$

Lean4

theorem bind_congr {s1 s2 : Computation α} {f1 f2 : α → Computation β} (h1 : s1 ~ s2) (h2 : ∀ a, f1 a ~ f2 a) :
    bind s1 f1 ~ bind s2 f2 := fun b =>
  ⟨fun h =>
    let ⟨a, ha, hb⟩ := exists_of_mem_bind h
    mem_bind ((h1 a).1 ha) ((h2 a b).1 hb),
    fun h =>
    let ⟨a, ha, hb⟩ := exists_of_mem_bind h
    mem_bind ((h1 a).2 ha) ((h2 a b).2 hb)⟩

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