powerset_cons — Mathlib

English

For any a and multiset s, the powerset of a appended to s equals the sum of the powerset of s and the image of powerset s under cons a.

Русский

Для любого элемента a и мультимножества s, powerset(a ⊎ s) есть сумма powerset(s) и образа powerset(s) под конструктором cons a.

LaTeX

$$$ \\mathrm{powerset}(a \\uplus s) = \\mathrm{powerset}(s) + \\mathrm{map}(\\mathrm{cons}\\ a)(\\mathrm{powerset}(s)) $$$

Lean4

@[simp]
theorem powerset_cons (a : α) (s) : powerset (a ::ₘ s) = powerset s + map (cons a) (powerset s) :=
  Quotient.inductionOn s fun l => by simp [Function.comp_def]

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