exists_of_mem_map — Mathlib

English

If b is in map f s, then there exists a in s with f a = b.

Русский

Если b ∈ map f s, то существует a ∈ s такой, что f a = b.

LaTeX

$$$$\forall f:\\alpha \to \\beta,\\forall b:\\beta,\\forall s:\\mathrm{WSeq}\\,\\alpha,\\text{b} \in \mathrm{map}\,f\,s \Rightarrow \exists a:\\alpha, a \in s \land f a = b.$$$$

Lean4

theorem exists_of_mem_map {f} {b : β} : ∀ {s : WSeq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b
  | ⟨g, al⟩, h => by
    let ⟨o, om, oe⟩ := Seq.exists_of_mem_map h
    rcases o with - | a
    · injection oe
    injection oe with h'
    exact ⟨a, om, h'⟩

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