mem_map — Mathlib

English

For any f: α → β, y ∈ o.map f holds exactly when there exists x ∈ o with f x = y.

Русский

Для любой функции f: α → β, y ∈ o.map f эквивалентно существованию x ∈ o такого, что f x = y.

LaTeX

$$$$ y \in o.map f \iff \exists x \in o, f x = y. $$$$

Lean4

theorem mem_map {f : α → β} {y : β} {o : Option α} : y ∈ o.map f ↔ ∃ x ∈ o, f x = y := by
  simp
    -- The simpNF linter says that the LHS can be simplified via `Option.mem_def`.
    -- However this is a higher priority lemma.
    -- It seems the side condition `H` is not applied by `simpNF`.
    -- https://github.com/leanprover/std4/issues/207

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