head — Mathlib

English

The head element of a Hindman finite-product sequence is contained in the Fred's FP set.

Русский

Головной элемент FP последовательности Хиндмана принадлежит множеству FP последовательности.

LaTeX

$$$\\text{head}(a) \\\\in FP(a)$.$$

Lean4

/-- Constructor for `FP`. This is the preferred spelling over `FP.head'`. -/
@[to_additive (attr := match_pattern, nolint defLemma) /--
    Constructor for `FS`. This is the preferred spelling over `FS.head'`. -/
    ]
abbrev head : a.head ∈ FP a :=
  FP.head' a

Похожие утверждения