surjOn_id

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.surjOn_id

English

For any set s, SurjOn id s s holds; the identity map is surjective on any s onto itself.

Русский

Для любого множества s отображение id обеспечивает SurjOn id s s.

LaTeX

$$$\\forall s:\\, \\mathrm{Set},\\ SurjOn\\ id\\ s\\ s.$$$

Lean4

theorem surjOn_id (s : Set α) : SurjOn id s s := by simp [SurjOn]

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

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

Разделы

Аффилиация

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