pi_cons — Mathlib

English

The pi-construction over the added element a to m is equal to the bind/map combination described by the standard Pi-cons decomposition.

Русский

Pi-cons над добавленным элементом a к m эквивалентен разложениям bind/map по стандартной схеме Pi-cons.

LaTeX

$$$\\forall m t a,\\; \\pi (a :: m) t = (t a).bind (\\lambda b, \\pi m t).\\mathrm{map} (\\Pi.cons m a b).$$$

Lean4

@[simp]
theorem pi_cons (m : Multiset α) (t : ∀ a, Multiset (β a)) (a : α) :
    pi (a ::ₘ m) t = (t a).bind fun b => (pi m t).map <| Pi.cons m a b :=
  recOn_cons a m

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