existsUnique — Mathlib

English

If f is bijective, then there exists a unique preimage for each target value: ∃! a with f(a) = b.

Русский

Если f биективна, то для каждого значения b найдется единственный предобраз a такой, что f(a)=b.

LaTeX

$$$\operatorname{Bijective}(f) \Rightarrow \forall b:\beta, \exists! a:\alpha, f(a)=b.$$$

Lean4

/-- Shorthand for using projection notation with `Function.bijective_iff_existsUnique`. -/
protected theorem existsUnique {f : α → β} (hf : Bijective f) (b : β) : ∃! a : α, f a = b :=
  (bijective_iff_existsUnique f).mp hf b

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