English
For any maps-to relation h, the injectivity of the restricted map h.restrict f s t is equivalent to injOn f s.
Русский
Для отображения h эквивалентно: инъективность h.restrict f s t равносильна injOn f s.
LaTeX
$$$\text{Injective}(h.restrict f s t) \iff \text{InjOn} f s$$$
Lean4
theorem restrict_inj (h : MapsTo f s t) : Injective (h.restrict f s t) ↔ InjOn f s := by
rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]