powersetCardAux_cons — Mathlib

English

powersetCardAux(n+1, a::l) = powersetCardAux(n+1, l) + map(cons a)(powersetCardAux(n, l)).

Русский

powersetCardAux(n+1, a::l) = powersetCardAux(n+1, l) + map(cons a)(powersetCardAux(n, l)).

LaTeX

$$powersetCardAux(n+1, List.cons(a,l)) = powersetCardAux(n+1, l) + List.map(Cons a) (powersetCardAux(n, l))$$

Lean4

@[simp]
theorem powersetCardAux_cons (n : ℕ) (a : α) (l : List α) :
    powersetCardAux (n + 1) (a :: l) = powersetCardAux (n + 1) l ++ List.map (cons a) (powersetCardAux n l) := by
  simp [powersetCardAux_eq_map_coe]

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