sublist_suffix_of_union — Mathlib

English

For lists l1 and l2, there exists a t such that t is a sublist of l1 and t ++ l2 equals l1 ∪ l2.

Русский

Для списков l1 и l2 существует t, такой что t является подпоследовательностью l1, и t ++ l2 = l1 ∪ l2.

LaTeX

$$$$ \\exists t:\\ t <+ l_1 \\land t \\;\\concat\\; l_2 = l_1 \\cup l_2. $$$$

Lean4

theorem sublist_suffix_of_union : ∀ l₁ l₂ : List α, ∃ t, t <+ l₁ ∧ t ++ l₂ = l₁ ∪ l₂
  | [], _ => ⟨[], by rfl, rfl⟩
  | a :: l₁, l₂ =>
    let ⟨t, s, e⟩ := sublist_suffix_of_union l₁ l₂
    if h : a ∈ l₁ ∪ l₂ then ⟨t, sublist_cons_of_sublist _ s, by simp only [e, cons_union, insert_of_mem h]⟩
    else ⟨a :: t, s.cons_cons _, by simp only [cons_append, cons_union, e, insert_of_not_mem h]⟩

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