bijOn_image

Mathlib.Data.Set.Function

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

English

If f is injective on s then f restricts to a bijection from s to its image f''s.

Русский

Если f инъективна на s, то ограничение f на s образует биекцию между s и изображением f(s).

LaTeX

$$$\\text{InjOn}(f,s)\\Rightarrow \\text{BijOn}(f,s,f''s)$$$

Lean4

theorem bijOn_image (h : InjOn f s) : BijOn f s (f '' s) :=
  BijOn.mk (mapsTo_image f s) h (Subset.refl _)

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

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

Разделы

Аффилиация

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