form_perm_zpow_apply_mem_imp_mem — Mathlib

English

If x ∈ l, then for every integer n, (formPerm l)^n x ∈ l.

Русский

Если x ∈ l, то для любого целого числа n (formPerm l)^n применимо к x остаётся в l.

LaTeX

$$$\forall {\alpha} [\DecidableEq \alpha],\ (l:\,\mathrm{List}\ \alpha),\ \mathrm{Membership}(l,x)\rightarrow\forall (n:\,\mathbb{Z}),\ (formPerm\ l\ ^ n) x \in l$$$

Lean4

theorem form_perm_zpow_apply_mem_imp_mem (l : List α) (x : α) (hx : x ∈ l) (n : ℤ) : (formPerm l ^ n) x ∈ l :=
  by
  by_cases h : (l.formPerm ^ n) x = x
  · simpa [h] using hx
  · have h : x ∈ {x | (l.formPerm ^ n) x ≠ x} := h
    rw [← set_support_apply_mem] at h
    replace h := set_support_zpow_subset _ _ h
    simpa using support_formPerm_le' _ h

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