infix_singleton_iff — Mathlib

English

For xs and x, xs is an infix of [x] if and only if xs is empty or xs = [x].

Русский

Для xs и x, xs является инфиксом [x] тогда и только тогда, когда xs пуст, или xs = [x].

LaTeX

$$$\forall {\alpha},\ xs:\, \text{List}(\alpha),\ x:\, \alpha,\; xs <:+: [x] \iff xs = \emptyset \text{ or } xs = [x].$$$

Lean4

theorem infix_singleton_iff (xs : List α) (x : α) : xs <:+: [x] ↔ xs = [] ∨ xs = [x] := by
  match xs with
  | [] => simp
  | [_] => simp [List.singleton_infix_singleton_iff]
  | _ :: _ :: _ =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · simp

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