Theorems · Theorem · logic and foundations
Set.Pairwise.imp
∀ {α : Type u_1} {r p : α → α → Prop} {s : Set α}, s.Pairwise r → (∀ ⦃a b : α⦄, r a b → p a b) → s.Pairwise p- Defined in
- Mathlib.Logic.Pairwise
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Pairwisestatement and proof · cited by 321
- Set.pairwise_of_forallproof · cited by 3
- Set.Pairwise.imp_onproof · cited by 3
Cited by14
Results whose statement or proof uses this declaration.
- Set.Pairwise.mono'proof · cited by 17
- Equiv.Perm.cycleType_eqproof · cited by 4
- MeasureTheory.addContent_biUnionproof · cited by 2
- Equiv.Perm.cycleType_eq'statement and proof · cited by 1
- Finset.sum_image_of_disjointproof · cited by 1
- Polynomial.quo_mul_prod_pow_add_sum_rem_mul_prod_pow_uniqueproof · cited by 1
- Equiv.Perm.Disjoint.cycleType_noncommProdstatement · cited by 1
- IsStrongAntichain.isAntichainproof · cited by 0
- Polynomial.natDegree_sum_eq_of_disjointproof · cited by 0
- Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_applyproof · cited by 0
- PiTensorProduct.tprod_noncommProdstatement · cited by 0
- Equiv.Perm.support_noncommProdstatement and proof · cited by 0