pi_insert — Mathlib

English

If a ∉ s, then pi(insert a s) t equals the biUnion over b ∈ t(a) of image of pi s t under Pi.cons s a b.

Русский

Если a ∉ s, то pi(insert a s) t равно объединению образов image (Pi.cons s a b) от (s.pi t) по всем b ∈ t(a).

LaTeX

$$$ pi (insert a s) t = (t a).biUnion (\\lambda b, pi s t).image (Pi.cons s a b). $$$

Lean4

@[simp]
theorem pi_insert [∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, Finset (β a)} {a : α} (ha : a ∉ s) :
    pi (insert a s) t = (t a).biUnion fun b => (pi s t).image (Pi.cons s a b) :=
  by
  apply eq_of_veq
  rw [← (pi (insert a s) t).2.dedup]
  refine
    (fun s' (h : s' = a ::ₘ s.1) =>
        (?_ :
          dedup (Multiset.pi s' fun a => (t a).1) =
            dedup
              ((t a).1.bind fun b =>
                dedup <|
                  (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' => Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
      _ (insert_val_of_notMem ha)
  subst s'; rw [pi_cons]
  congr; funext b
  exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm

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