singleton_infix_iff — Mathlib

English

For any x and xs, [x] is an infix of xs if and only if x belongs to xs.

Русский

Для любых x и xs, [x] является инфиксом xs тогда и только тогда, когда x принадлежит xs.

LaTeX

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

Lean4

theorem singleton_infix_iff (x : α) (xs : List α) : [x] <:+: xs ↔ x ∈ xs :=
  by
  rw [List.mem_iff_append, List.IsInfix]
  congr! 4
  simp [eq_comm]

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