exists_of_mem_bind — Mathlib

English

If b ∈ bind s f, then there exists a ∈ s with b ∈ f a.

Русский

Если b ∈ bind s f, тогда существует a ∈ s such that b ∈ f a.

LaTeX

$$$$ b \\in (s \\mathbin{\\text{bind}} f) \\Rightarrow \\exists a \\in s, b \\in f(a) $$$$

Lean4

theorem exists_of_mem_bind {s : WSeq α} {f : α → WSeq β} {b} (h : b ∈ bind s f) : ∃ a ∈ s, b ∈ f a :=
  let ⟨t, tm, bt⟩ := exists_of_mem_join h
  let ⟨a, as, e⟩ := exists_of_mem_map tm
  ⟨a, as, by rwa [e]⟩

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