Theorems · Theorem · combinatorics
Finset.monotone_filter_right
∀ {α : Type u_1} (s : Finset α) ⦃p q : α → Prop⦄ [inst : DecidablePred p] [inst_1 : DecidablePred q],
(∀ a ∈ s, p a → q a) → Finset.filter p s ⊆ Finset.filter q s- Defined in
- Mathlib.Data.Finset.Filter
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidablePredDecidablePred
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.filterstatement · cited by 949
Cited by10
Results whose statement or proof uses this declaration.
- hammingDist_comp_le_hammingDistproof · cited by 3
- hammingDist_triangleproof · cited by 2
- hammingDist_compproof · cited by 2
- Nat.primeCounting'_add_leproof · cited by 1
- Finpartition.nonUniforms_monoproof · cited by 1
- SimpleGraph.regularityReduced_edges_card_auxproof · cited by 1
- sum_div_nat_floor_pow_sq_le_div_sqproof · cited by 1
- schnirelmannDensity_le_of_subsetproof · cited by 0
- SimpleGraph.cliqueFinset_monoproof · cited by 0
- Finpartition.sparsePairs_monoproof · cited by 0