infix_flatMap_of_mem — Mathlib

English

If a ∈ as, then f a appears as an infix element of as.flatMap f.

Русский

Если a принадлежит as, то элемент f(a) появляется в as.flatMap f как инфикс.

LaTeX

$$$\\\\forall {a:\\\\alpha} {as:\\\\text{List }\\\\alpha},\\\\, a \\\\in as \\\\Rightarrow \\\\exists p,q:\\\\text{List }\\\\beta,\\\\ as.flatMap f = p \\\\fbox{ }\\, [f(a)] \\\\q$$

Lean4

theorem infix_flatMap_of_mem {a : α} {as : List α} (h : a ∈ as) (f : α → List α) : f a <:+: as.flatMap f :=
  infix_of_mem_flatten (mem_map_of_mem h)

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