mem_range_iff_existsUnique — Mathlib

English

Let f: A → B be injective. For every b ∈ B, b ∈ range(f) iff there exists exactly one a ∈ A with f(a) = b.

Русский

Пусть f: A → B инъективна. Для каждого b ∈ B верно: b принадлежит образу f тогда и только тогда существует ровно один a ∈ A such that f(a) = b.

LaTeX

$$$b \in \operatorname{range}(f) \iff \exists! a\, f(a)=b$$$

Lean4

theorem mem_range_iff_existsUnique (hf : Injective f) {b : β} : b ∈ range f ↔ ∃! a, f a = b :=
  ⟨fun ⟨a, h⟩ => ⟨a, h, fun _ ha => hf (ha.trans h.symm)⟩, ExistsUnique.exists⟩

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