Equivalence between Finset.finsuppAntidiag and Sym

This file collects further results about equivalence and cardinality related to Finset.finsuppAntidiag. This file is separated from Mathlib.Algebra.Order.Antidiag.Finsupp to reduce imports.

Main declarations

• Finset.finsuppAntidiagEquivSubtype: Finset.finsuppAntidiag s n is equivalent to subtype of s →₀ μ whose sum is n.
• Finset.finsuppAntidiagEquiv: Finset.finsuppAntidiag s n is equivalent to Sym s n for natural number n.
• Finset.card_finsuppAntidiag_nat_eq_choose and Finset.card_finsuppAntidiag_nat_eq_multichoose: cardinality formula for Finset.finsuppAntidiag s n for natural number n.

noncomputable def Finset.finsuppAntidiagEquivSubtype {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) (n : μ) : ↥(s.finsuppAntidiag n) ≃ { P : ↥s →₀ μ // (P.sum fun (x : ↥s) => id) = n }

The equivalence between Finset.finsuppAntidiag s n and the subtype of s →₀ μ whose sum is n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finset.finsuppAntidiagEquivSubtype_apply_coe {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) (n : μ) (f : ↥(s.finsuppAntidiag n)) : ↑((s.finsuppAntidiagEquivSubtype n) f) = Finsupp.subtypeDomain (fun (x : ι) => x ∈ s) ↑f

@[simp]

theorem Finset.finsuppAntidiagEquivSubtype_symm_apply_coe {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) (n : μ) (f : { P : ↥s →₀ μ // (P.sum fun (x : ↥s) => id) = n }) : ↑((s.finsuppAntidiagEquivSubtype n).symm f) = (↑f).extendDomain

noncomputable def Finset.finsuppAntidiagEquiv {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (n : ℕ) : ↥(s.finsuppAntidiag n) ≃ Sym (↥s) n

The equivalence between Finset.finsuppAntidiag s n and Sym s n.

Equations

• s.finsuppAntidiagEquiv n = (s.finsuppAntidiagEquivSubtype n).trans (Sym.equivNatSum (↥s) n).symm

@[simp]

theorem Finset.finsuppAntidiagEquiv_symm_apply_apply {ι : Type u_1} [DecidableEq ι] {s : Finset ι} (n : ℕ) (f : Sym (↥s) n) (a : ↥s) : ↑((s.finsuppAntidiagEquiv n).symm f) ↑a = Multiset.count a ↑f

@[simp]

theorem Finset.count_coe_finsuppAntidiagEquiv_apply {ι : Type u_1} [DecidableEq ι] {s : Finset ι} (n : ℕ) (f : ↥(s.finsuppAntidiag n)) (a : ↥s) : Multiset.count a ↑((s.finsuppAntidiagEquiv n) f) = ↑f ↑a

theorem Finset.card_finsuppAntidiag_nat_eq_choose {ι : Type u_1} [DecidableEq ι] {s : Finset ι} (n : ℕ) : (s.finsuppAntidiag n).card = (s.card + n - 1).choose n

theorem Finset.card_finsuppAntidiag_nat_eq_multichoose {ι : Type u_1} [DecidableEq ι] {s : Finset ι} (n : ℕ) : (s.finsuppAntidiag n).card = s.card.multichoose n