bind_congr'' — Mathlib

English

For any x and functions f,g with equal behavior on all elements of x, x.bind f = x.bind g.

Русский

Для любого x и функций f,g такие, что они ведут себя одинаково на всех элементах x, выполняется x.bind f = x.bind g.

LaTeX

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

Lean4

@[deprecated bind_congr (since := "2025-03-20")]
  -- This was renamed from `bind_congr` after https://github.com/leanprover/lean4/pull/7529
  -- upstreamed it with a slightly different statement.

theorem bind_congr'' {f g : α → Option β} {x : Option α} (h : ∀ a ∈ x, f a = g a) : x.bind f = x.bind g := by
  grind [cases Option]

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