comp_injOn

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Function.Injective.comp_injOn

English

If g is injective and f is injective on s, then g∘f is injective on s.

Русский

Если g инъективна и f инъективна на s, то композиция g∘f инъективна на s.

LaTeX

$$$(hg : Injective g) \\to (hf : s.InjOn f) \\\\Rightarrow s.InjOn (g \\circ f)$$$

Lean4

theorem comp_injOn (hg : Injective g) (hf : s.InjOn f) : s.InjOn (g ∘ f) :=
  hg.injOn.comp hf (mapsTo_univ _ _)

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

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

Разделы

Аффилиация

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