map_eq_one_iff — Mathlib

English

Let f: α → β and v ∈ WithTop α. Then map f v equals 1 if and only if there exists x such that v = some x and f x = 1.

Русский

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

LaTeX

$$$\\mathrm{WithTop.map}\\ f\\ v = 1 \\iff \\exists x:\\alpha,\\ v = \\mathrm{WithTop}.some\\ x \\land f x = 1$$$

Lean4

@[to_additive]
theorem map_eq_one_iff {α} {f : α → β} {v : WithTop α} [One β] : WithTop.map f v = 1 ↔ ∃ x, v = .some x ∧ f x = 1 :=
  map_eq_some_iff

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