coe_powerset — Mathlib

English

The powerset, viewed as a set of Finsets, corresponds to the preimage of the powerset of s under the inclusion map.

Русский

Очевидно: множество подмножеств s соответствует предобразованию множества подмножеств s под включением.

LaTeX

$$$$ (s.powerset : \\text{Set}(\\text{Finset} \\; \\alpha)) = (\\uparrow : \\text{Finset } \\alpha \\to \\text{Set} \\ \\alpha)^{-1} \\bigl( (s: \\text{Set } \\alpha).powerset \\bigr). $$$$

Lean4

@[simp, norm_cast]
theorem coe_powerset (s : Finset α) :
    (s.powerset : Set (Finset α)) = ((↑) : Finset α → Set α) ⁻¹' (s : Set α).powerset :=
  by
  ext
  simp

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