Theorems · Theorem · combinatorics
Finsupp.image_prodMap_embDomain_antidiagonal
∀ {α : Type u} [inst : DecidableEq α] {β : Type u_1} [inst_1 : DecidableEq β] (f : α ↪ β) (y : α →₀ ℕ),
Finset.image (Prod.map (Finsupp.embDomain f) (Finsupp.embDomain f)) (Finset.HasAntidiagonal.antidiagonal y) =
Finset.HasAntidiagonal.antidiagonal (Finsupp.embDomain f y)- Defined in
- Mathlib.Data.Finsupp.Antidiagonal
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsetstatement · cited by 13,712
- Finsuppstatement and proof · cited by 5,255
- Function.Embeddingstatement and proof · cited by 988
- Finset.imagestatement · cited by 910
- Finset.extproof · cited by 565
- Function.Injective.injOnproof · cited by 280
- Finset.HasAntidiagonal.antidiagonalstatement · cited by 218
- Function.Embedding.injectiveproof · cited by 111
- Finsupp.embDomainstatement and proof · cited by 69
- Finsupp.comapDomainproof · cited by 40
- le_iff_exists_addproof · cited by 16
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.