injOn_iff_injective — Mathlib

English

For a function f and a set s, f injOn s is equivalent to the restriction s.restrict f being injective.

Русский

Для функции f и множества s условие injOn f s эквивалентно тому, что ограничение s.restrict f инъективно.

LaTeX

$$$\operatorname{InjOn} f s \;\iff\; \operatorname{Injective}(s.restrict f)$$$

Lean4

theorem injOn_iff_injective : InjOn f s ↔ Injective (s.restrict f) :=
  ⟨fun H a b h => Subtype.eq <| H a.2 b.2 h, fun H a as b bs h => congr_arg Subtype.val <| @H ⟨a, as⟩ ⟨b, bs⟩ h⟩

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