mem_map_iff — Mathlib

English

For c, f, and b, b ∈ c.map f iff ∃ a ∈ c with f(a) = b.

Русский

Для цепи c, отображения f и элемента b: b ∈ c.map f тогда и только тогда, когда ∃ a ∈ c, f(a) = b.

LaTeX

$$$ b \\in c.map f \\iff \\exists a \\in c, f(a) = b $$$

Lean4

@[simp]
theorem mem_map_iff {b : β} : b ∈ c.map f ↔ ∃ a, a ∈ c ∧ f a = b :=
  ⟨exists_of_mem_map _, fun h => by
    rcases h with ⟨w, h, h'⟩
    subst b
    apply mem_map c _ h⟩

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