surjective_iff_bijective

Mathlib.Data.Fintype.Card

URI: https://scilib.ai/kg/mathlib#Finite.surjective_iff_bijective

English

For a finite α, a function f: α → α is surjective if and only if it is bijective.

Русский

Для конечного α функция f: α → α сюръективна тогда и только тогда, когда она биективна.

LaTeX

$$Surjective f ↔ Bijective f$$

Lean4

theorem surjective_iff_bijective {f : α → α} : Surjective f ↔ Bijective f := by
  simp [Bijective, injective_iff_surjective]

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

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

Разделы

Аффилиация

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