injective_rangeRestrict_iff

Mathlib.Algebra.Module.Submodule.Range

URI: https://scilib.ai/kg/mathlib#LinearMap.injective_rangeRestrict_iff

English

The map f.rangeRestrict is injective if and only if f is injective.

Русский

Отображение f.rangeRestrict инъективно тогда и только тогда, когда f инъективно.

LaTeX

$$$$\\operatorname{Injective}(f.\\mathrm{rangeRestrict}) \\iff \\operatorname{Injective}(f).$$$$

Lean4

@[simp]
theorem injective_rangeRestrict_iff : Injective f.rangeRestrict ↔ Injective f :=
  Set.injective_codRestrict _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru