English
If f is injective, then the partial inverse of f is a partial inverse of f.
Русский
Если f инъективна, то частичное обратное к f является частичным обратным к f.
LaTeX
$$$ \text{Injective}(f) \rightarrow \text{IsPartialInv}(f, \mathrm{partialInv}(f)) $$$
Lean4
theorem partialInv_of_injective {α β} {f : α → β} (I : Injective f) : IsPartialInv f (partialInv f)
| a, b =>
⟨fun h =>
open scoped Classical in
have hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none := rfl
if h' : ∃ a, f a = b then by
rw [hpi, dif_pos h'] at h
injection h with h
subst h
apply Classical.choose_spec h'
else by rw [hpi, dif_neg h'] at h; contradiction,
fun e =>
e ▸
have h : ∃ a', f a' = f a := ⟨_, rfl⟩
(dif_pos h).trans (congr_arg _ (I <| Classical.choose_spec h))⟩
