mapsTo_of_subsingleton

Mathlib.Data.Set.Function

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

English

If α is a subsingleton, then any f: α → α maps any s to itself, i.e., MapsTo f s s.

Русский

Если α — подмножество-одиночное, то любое отображение f: α→α отображает s в s.

LaTeX

$$$ [Subsingleton\\alpha] (f: \\alpha \\to \\alpha) (s: Set\\alpha) : MapsTo f s s $$$

Lean4

theorem mapsTo_of_subsingleton [Subsingleton α] (f : α → α) (s : Set α) : MapsTo f s s :=
  mapsTo_of_subsingleton' _ id

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

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

Разделы

Аффилиация

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