map_eq_some_iff — Mathlib

English

Let f: α → β and v ∈ WithBot α. Then WithBot.map f v equals some y if and only if there exists x with v = some x and f x = y.

Русский

Пусть f: α → β и v ∈ WithBot α. Тогда WithBot.map f v равно some y тогда и только тогда существует x такое, что v = some x и f x = y.

LaTeX

$$$WithBot.map f v = \mathrm{some} y \iff \exists x, v = \mathrm{some} x \land f x = y$$$

Lean4

theorem map_eq_some_iff {f : α → β} {y : β} {v : WithBot α} : WithBot.map f v = .some y ↔ ∃ x, v = .some x ∧ f x = y :=
  Option.map_eq_some_iff

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