some_eq_map_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem some_eq_map_iff {f : α → β} {y : β} {v : WithBot α} : .some y = WithBot.map f v ↔ ∃ x, v = .some x ∧ f x = y :=
  by cases v <;> simp [eq_comm]

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