exists_of_mem_map — Mathlib

English

If b ∈ map f s, there exists a with a ∈ s and f a = b.

Русский

Если b ∈ map f s, существует a ∈ s и f a = b.

LaTeX

$$$ b \in \operatorname{map} f\, s \Rightarrow \exists a \in s, f a = b$$$

Lean4

theorem exists_of_mem_map {f : α → β} {b : β} {s : Computation α} (h : b ∈ map f s) : ∃ a, a ∈ s ∧ f a = b :=
  by
  rw [← bind_pure] at h
  let ⟨a, as, fb⟩ := exists_of_mem_bind h
  exact ⟨a, as, mem_unique (ret_mem _) fb⟩

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