sigma_preimage_mk — Mathlib

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]

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