some_eq_map_iff — Mathlib

English

Equality of Some y with map f v is equivalent to existence of x with v=Some x and f x = y.

Русский

Равенство Some(y) и map f v эквивалентно существованию x с v=Some x и f x = y.

LaTeX

$$$\\mathrm{Some}(y) = \\mathrm{WithTop.map}\\ f\\ v \\iff \\exists x,\\ v = \\mathrm{Some}(x) \\land f(x) = y$$$

Lean4

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

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