eq_or_mem_of_mem_cons — Mathlib

English

Let a,b ∈ α and s ∈ Seq α. If a belongs to cons(b,s), then either a = b or a ∈ s.

Русский

Пусть a,b ∈ α и s ∈ Seq α. Если a принадлежит cons(b,s), тогда либо a = b, либо a ∈ s.

LaTeX

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

Lean4

theorem eq_or_mem_of_mem_cons {a b : α} : ∀ {s : Seq α}, a ∈ cons b s → a = b ∨ a ∈ s
  | ⟨_, _⟩, h => (Stream'.eq_or_mem_of_mem_cons h).imp_left fun h => by injection h

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