mono_sublist — Mathlib

English

If x occurs in l and l is a sublist of l', then x occurs in l'.

Русский

Если x встречается в l и l является подсписком под l', то x встречается в l'.

LaTeX

$$$ x \in+ l \land l \lessdot l' \Rightarrow x \in+ l' $$$

Lean4

theorem mono_sublist {l' : List α} (hx : x ∈+ l) (h : l <+ l') : x ∈+ l' := by
  induction h with
  | slnil => exact hx
  | cons y _ IH => exact (IH hx).duplicate_cons _
  | cons₂ y h IH =>
    rw [duplicate_cons_iff] at hx ⊢
    rcases hx with (⟨rfl, hx⟩ | hx)
    · simp [h.subset hx]
    · simp [IH hx]

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