first_mem_of_cons_mem_sym — Mathlib

English

If a ::ₛ z ∈ xs.sym (n + 1), then a ∈ xs.

Русский

Если элемент a с символом z стоит на первом месте и принадлежит xs.sym (n + 1), то a принадлежит xs.

LaTeX

$$$ a ::_s z \in xs.sym (n + 1) \Rightarrow a \in xs $$$

Lean4

theorem first_mem_of_cons_mem_sym {xs : List α} {n : ℕ} {a : α} {z : Sym α n} (h : a ::ₛ z ∈ xs.sym (n + 1)) : a ∈ xs :=
  mem_of_mem_of_mem_sym (Sym.mem_cons_self a z) h

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