image_of_comp

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.InjOn.image_of_comp

← MathLib Explorer

English

If InjOn (g ∘ f) s, then InjOn g (f '' s).

Русский

Если InjOn (g ∘ f) на s, тогда InjOn g на образе f(s).

LaTeX

$$$ \\operatorname{InjOn}(g \\circ f) s \\Rightarrow \\operatorname{InjOn} g (f'' s)$$

Lean4

theorem image_of_comp (h : InjOn (g ∘ f) s) : InjOn g (f '' s) :=
  forall_mem_image.2 fun _x hx ↦ forall_mem_image.2 fun _y hy heq ↦ congr_arg f <| h hx hy heq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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