sigma_preimage_mk_of_subset — Mathlib

English

If the projection image of s lies inside t, then the sigma construction equals s.

Русский

Если образ проекции множества s лежит внутри t, то сигма-конструкция равна s.

LaTeX

$$$$ (t.\\sigma (a \\mapsto s.preimage (\\Sigma.mk a) \\mathrm{injOn})) = s $$$$

Lean4

theorem sigma_preimage_mk_of_subset {β : α → Type*} [DecidableEq α] (s : Finset (Σ a, β a)) {t : Finset α}
    (ht : s.image Sigma.fst ⊆ t) : (t.sigma fun a => s.preimage (Sigma.mk a) sigma_mk_injective.injOn) = s := by
  rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]

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