English
For a family of finite sets indexed by α, the sigma-construction over α with the preimages of each a yields a Finset isomorphic to the σ-structure restricted to s.
Русский
Для семейства конечных множеств, индексационных по α, сигма‑конструкция над α с предобразами каждого a эквивалентна σ‑структуре, ограниченной множеством s.
LaTeX
$$$$ t.\\sigma\\bigl( a \\mapsto s.preimage (\\Sigma.mk a) \\mathrm{injOn} \\bigr) = \\{ a \\in s \\mid a.1 \\in t \\}. $$$$
Lean4
theorem sigma_preimage_mk {β : α → Type*} [DecidableEq α] (s : Finset (Σ a, β a)) (t : Finset α) :
t.sigma (fun a => s.preimage (Sigma.mk a) sigma_mk_injective.injOn) = {a ∈ s | a.1 ∈ t} :=
by
ext x
simp [and_comm]