restrict_inj — Mathlib

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]

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