English
If the forward direction is defined for all inputs except a fixed a₂, then the forward function is injective.
Русский
Если для всех аргументов кроме фиксированного a₂ отображение вперёд определено, тогда функция является инъективной.
LaTeX
$$$$ \\text{Injective}(f) \\text{ if } \\forall a_1\\neq a_2,\\ isSome(f(a_1)). $$$$
Lean4
/-- If the domain of a `PEquiv` is `α` except a point, its forward direction is injective. -/
theorem injective_of_forall_ne_isSome (f : α ≃. β) (a₂ : α) (h : ∀ a₁ : α, a₁ ≠ a₂ → isSome (f a₁)) : Injective f :=
HasLeftInverse.injective
⟨fun b => Option.recOn b a₂ fun b' => Option.recOn (f.symm b') a₂ id, fun x => by
classical
cases hfx : f x
· have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)
simp [this]
· dsimp only
rw [(eq_some_iff f).2 hfx]
rfl⟩
