mem_cons_of_mem — Mathlib

English

Let a and y be elements of a type α, and s be a sequence of α. If a is in s, then a is in the sequence obtained by prepending y to s.

Русский

Пусть a и y принадлежат множеству α, и пусть s — последовательность элементов α. Если a ∈ s, то a ∈ cons(y, s).

LaTeX

$$$ \forall y \in \alpha\,\forall a \in \alpha\, \forall s \in \mathrm{Seq}(\alpha),\ a \in s \Rightarrow a \in \mathrm{cons}(y,s).$$$

Lean4

theorem mem_cons_of_mem (y : α) {a : α} : ∀ {s : Seq α}, a ∈ s → a ∈ cons y s
  | ⟨_, _⟩ => Stream'.mem_cons_of_mem (some y)

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