preimage_surjective

Mathlib.Data.Set.Image

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

English

If f is injective, then the preimage map is surjective.

Русский

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

LaTeX

$$$(hf: Injective f) \Rightarrow \text{Surjective} (\text{preimage } f).$$$

Lean4

theorem preimage_surjective (hf : Injective f) : Surjective (preimage f) :=
  Set.preimage_surjective.mpr hf

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

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

Разделы

Аффилиация

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