bind_congr' — Mathlib

English

If x = y and hf ensures f and g agree on y, then x.bind f = y.bind g.

Русский

Если x = y и hf гарантирует, что f и g совпадают на y, то x.bind f = y.bind g.

LaTeX

$$$$ x = y \Rightarrow (\forall a \in y, f a = g a) \Rightarrow x.\bind f = y.\bind g. $$$$

Lean4

@[congr]
theorem bind_congr' {f g : α → Option β} {x y : Option α} (hx : x = y) (hf : ∀ a ∈ y, f a = g a) :
    x.bind f = y.bind g :=
  hx.symm ▸ bind_congr hf

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