injective_of_forall_isSome — Mathlib

English

If f maps every input to some value, then f is injective.

Русский

Если для каждого входа существует образ, то функция инъективна.

LaTeX

$$$$ \\forall a, \\text{isSome}(f(a)) \\Rightarrow \\text{Injective}(f). $$$$

Lean4

/-- If the domain of a `PEquiv` is all of `α`, its forward direction is injective. -/
theorem injective_of_forall_isSome {f : α ≃. β} (h : ∀ a : α, isSome (f a)) : Injective f :=
  (Classical.em (Nonempty α)).elim (fun hn => injective_of_forall_ne_isSome f (Classical.choice hn) fun a _ => h a)
    fun hn x => (hn ⟨x⟩).elim

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