sigma — Mathlib

English

If s is nodup and each t(a) is nodup, then s.sigma t is nodup.

Русский

Если s без повторов и каждый t(a) без повторов, то s.sigma t без повторов.

LaTeX

$$$s.\mathrm{Nodup} \to (\forall a, (t a).Nodup) \to (s.\sigma t).Nodup$$$

Lean4

protected theorem sigma {σ : α → Type*} {t : ∀ a, Multiset (σ a)} : Nodup s → (∀ a, Nodup (t a)) → Nodup (s.sigma t) :=
  Quot.induction_on s fun l₁ => by
    choose f hf using fun a => Quotient.exists_rep (t a)
    simpa [← funext hf] using List.Nodup.sigma

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