exists_of_mem_map — Mathlib

English

If b belongs to map f s, there exists a in s such that f a = b.

Русский

Если b принадлежит map f s, существует a в s такое, что f a = b.

LaTeX

$$$\forall {f} {b} {s : Seq \alpha}, b \in map f s \Rightarrow \exists a, a \in s \land f a = b$$$

Lean4

theorem exists_of_mem_map {f} {b : β} : ∀ {s : Seq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b := fun {s} h => by
  match s with
  | ⟨g, al⟩ =>
    let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
    rcases o with - | a
    · injection oe
    · injection oe with h'; exact ⟨a, om, h'⟩

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