Theorems · Theorem · combinatorics
Finset.forall_mem_cons
∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) (p : α → Prop), (∀ x ∈ Finset.cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x- Defined in
- Mathlib.Data.Finset.Insert
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
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.consstatement · cited by 221
Cited by12
Results whose statement or proof uses this declaration.
- logDeriv_prodproof · cited by 4
- MeasureTheory.integral_finsetSum_measureproof · cited by 4
- Filter.Tendsto.finset_sup'_nhdsproof · cited by 4
- IsCoprime.prod_leftproof · cited by 3
- Real.rpow_sum_of_nonnegproof · cited by 2
- Finset.inf_inductionproof · cited by 2
- Polynomial.quo_mul_prod_add_sum_rem_mul_prod_uniqueproof · cited by 1
- Set.PartiallyWellOrderedOn.piproof · cited by 1
- Polynomial.eq_quo_mul_prod_add_sum_rem_mul_prodproof · cited by 1
- WellQuasiOrdered.piproof · cited by 0
- ENat.iInf_sumproof · cited by 0
- ENNReal.iInf_sumproof · cited by 0