FP_drop_subset_FP — Mathlib

English

In any semigroup, FP-set of the tail after dropping n elements is contained in FP a: FP (a.drop n) ⊆ FP a.

Русский

В любом полугруппе FP‑множество хвоста после удаления первых n элементов содержится в FP a: FP(a.drop n) ⊆ FP(a).

LaTeX

$$$$ \forall {M} [Semigroup M] (a : Stream' M) (n : \mathbb{N}), FP(a.drop n) \subseteq FP a $$$$

Lean4

@[to_additive FS_iter_tail_sub_FS]
theorem FP_drop_subset_FP {M} [Semigroup M] (a : Stream' M) (n : ℕ) : FP (a.drop n) ⊆ FP a := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [← Stream'.drop_drop]
    exact _root_.trans (FP.tail _) ih

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