Mathlib Map

Theorems · Definition · combinatorics

Hindman.FP.tail

∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (m : M), Hindman.FP a.tail m → m ∈ Hindman.FP a

Constructor for FP. This is the preferred spelling over FP.tail'.

Defined in
Mathlib.Combinatorics.Hindman
Cited by
4 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Assumes
Semigroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Hindman.FP_drop_subset_FP · cited by 2Hindman.FP_drop_subset_FPHindman.exists_idempotent_ultrafilter_le_FP · cited by 1Hindman.exists_idempotent…Hindman.FP.singleton · cited by 1FP.singletonHindman.FP.mul · cited by 1FP.mulSet · cited by 53352SetStream' · cited by 205Stream'Semigroup · cited by 202SemigroupStream'.tail · cited by 68Stream'.tailHindman.FP · cited by 11Hindman.FPFP.tailCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Stream'statement and proof · cited by 205
  • Semigroupstatement and proof · cited by 202
  • Stream'.tailstatement and proof · cited by 68
  • Hindman.FPstatement and proof · cited by 11

Cited by4

Results whose statement or proof uses this declaration.