mem_append_left

Mathlib.Data.Seq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.mem_append_left

English

If a is a member of s1, then a is a member of append s1 s2.

Русский

Если a принадлежит s1, то a принадлежит append s1 s2.

LaTeX

$$$\forall {s_1 s_2 : Seq \alpha} \; a \in s_1 \Rightarrow a \in append s_1 s_2$$$

Lean4

theorem mem_append_left {s₁ s₂ : Seq α} {a : α} (h : a ∈ s₁) : a ∈ append s₁ s₂ := by apply mem_rec_on h; intros;
  simp [*]

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

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

Разделы

Аффилиация

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