injOn_of_injective

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.injOn_of_injective

English

If f is injective, then f is injective on any subset s of its domain.

Русский

Если f инъективна, то она инъективна на любом подмножестве s своей области определения.

LaTeX

$$$ \\operatorname{Injective}(f) \\Rightarrow \\forall s\\, \\operatorname{InjOn}(f,s)$$$

Lean4

theorem injOn_of_injective (h : Injective f) {s : Set α} : InjOn f s := fun _ _ _ _ hxy => h hxy

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

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

Разделы

Аффилиация

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