map_eq_one_iff — Mathlib

English

For any f: α → β and v ∈ WithBot α, with 1 in β, WithBot.map f v = 1 holds iff there exists x with v = some x and f x = 1.

Русский

Для любого отображения f: α → β и v ∈ WithBot α, если β имеет единицу, то WithBot.map f v = 1 эквивалентно существованию x такого, что v = some x и f x = 1.

LaTeX

$$$ \\forall {β} {α} {f : α \\to β} {v : \\mathrm{WithBot}\\,\\alpha} [1_β], \\mathrm{WithBot.map}\, f\, v = 1 \\iff \\exists x, v = \\mathrm{WithBot.some}\\ x \\land f\\,x = 1 $$$

Lean4

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

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