Theorems · Definition · combinatorics
Finset.Nat.sigmaAntidiagonalTupleEquivTuple
(k : ℕ) → (n : ℕ) × ↥(Finset.Nat.antidiagonalTuple k n) ≃ (Fin k → ℕ)
The disjoint union of antidiagonal tuples Σ n, antidiagonalTuple k n is equivalent to the
k-tuple Fin k → ℕ. This is such an equivalence, obtained by mapping (n, x) to x.
This is the tuple version of Finset..HasAntidiagonal.sigmaAntidiagonalEquivProd.
- Defined in
- Mathlib.Data.Fin.Tuple.NatAntidiagonal
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Equivstatement · cited by 8,337
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- Finset.Nat.antidiagonalTuplestatement and proof · cited by 10
Cited by3
Results whose statement or proof uses this declaration.
- Finset.Nat.sigmaAntidiagonalTupleEquivTuple_applystatement and proof · cited by 0
- Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fststatement and proof · cited by 0
- Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coestatement and proof · cited by 0