sigma_image_fst_preimage_mk — Mathlib

English

The preimage of the left injection Sum.inl is precisely the left part of the sum.

Русский

Предобраз Sum.inl равен левой части суммы.

LaTeX

$$$$ s.preimage (\\mathrm{Sum.inl}) (\\mathrm{Sum.inl_injective}.injOn) = s^{\\text{toLeft}}. $$$$

Lean4

theorem sigma_image_fst_preimage_mk {β : α → Type*} [DecidableEq α] (s : Finset (Σ a, β a)) :
    ((s.image Sigma.fst).sigma fun a => s.preimage (Sigma.mk a) sigma_mk_injective.injOn) = s :=
  s.sigma_preimage_mk_of_subset (Subset.refl _)

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