of_mem_append

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.of_mem_append

English

If a belongs to the concatenation append s1 s2, then a belongs to s1 or to s2.

Русский

Если a ∈ append s1 s2, тогда a ∈ s1 или a ∈ s2.

LaTeX

$$$$\forall s_1 s_2:\\mathrm{WSeq}\,\alpha,\forall a:\\alpha,\ a \in \mathrm{append}\,s_1\,s_2 \Rightarrow a \in s_1 \lor a \in s_2.$$$$

Lean4

theorem of_mem_append {s₁ s₂ : WSeq α} {a : α} : a ∈ append s₁ s₂ → a ∈ s₁ ∨ a ∈ s₂ :=
  Seq.of_mem_append

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru