English
Let f be a function from the option type to some set. Then f is injective iff its restriction to the Some-part is injective and the value at None does not belong to the range of that restriction.
Русский
Пусть f: Option A → B. Тогда f инъективна тогда и только тогда, когда её ограничение на часть Some является инъективной, и значение в None не принадлежит области значений этого ограничения.
LaTeX
$$$\operatorname{Injective}(f) \iff \big( \operatorname{Injective}(f \circ \mathrm{Some}) \land f(\mathrm{None}) \notin \operatorname{range}(f \circ \mathrm{Some}) \big)$$$
Lean4
theorem injective_iff {α β} {f : Option α → β} : Injective f ↔ Injective (f ∘ some) ∧ f none ∉ range (f ∘ some) :=
by
simp only [mem_range, not_exists, (· ∘ ·)]
refine ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩
rintro ⟨h_some, h_none⟩ (_ | a) (_ | b) hab
exacts [rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)]
