Theorems · Theorem · combinatorics
Set.VAddAntidiagonal.finite_of_isPWO
∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} [inst : PartialOrder G] [inst_1 : PartialOrder P]
[inst_2 : VAdd G P] [IsOrderedCancelVAdd G P], s.IsPWO → t.IsPWO → ∀ (a : P), (s.vaddAntidiagonal t a).Finite- Defined in
- Mathlib.Data.Set.SMulAntidiagonal
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- PartialOrderstatement and proof · cited by 6,410
- LT.lt.leproof · cited by 2,189
- Set.Finitestatement and proof · cited by 1,814
- LT.lt.neproof · cited by 872
- OrderEmbeddingproof · cited by 619
- VAddstatement and proof · cited by 616
- Function.Embedding.injectiveproof · cited by 111
- Set.IsPWOstatement and proof · cited by 99
- Subrelproof · cited by 53
- Order.Preimageproof · cited by 42
Cited by16
Results whose statement or proof uses this declaration.
- HahnModule.coeff_smulstatement · cited by 5
- HahnSeries.SummableFamily.smul_hsumproof · cited by 2
- HahnModule.coeff_single_smul_vaddproof · cited by 2
- HahnModule.coeff_smul_leftstatement and proof · cited by 2
- HahnModule.coeff_smul_rightstatement and proof · cited by 2
- HahnSeries.SummableFamily.coeff_smulstatement and proof · cited by 2
- HahnModule.zero_smul'proof · cited by 2
- Finset.vaddAntidiagonal_min_vadd_minstatement and proof · cited by 1
- HahnSeries.SummableFamily.sum_vAddAntidiagonal_eqstatement and proof · cited by 1
- HahnModule.coeff_smul_order_add_orderproof · cited by 1
- HahnSeries.SummableFamily.isPWO_iUnion_support_prod_smulproof · cited by 1
- HahnModule.support_smul_subset_vadd_support'proof · cited by 1