of_subsingleton

Mathlib.Logic.Function.Defs

URI: https://scilib.ai/kg/mathlib#Function.IsFixedPt.of_subsingleton

English

If α is a Subsingleton, then for any f: α → α and any x ∈ α, x is a fixed point of f.

Русский

Если α — одноэлементное множество, то для любого f: α → α и любого x ∈ α, x является фиксированной точкой f.

LaTeX

$$$ \text{IsFixedPt}(f,x) $$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton α] (f : α → α) (x : α) : IsFixedPt f x :=
  Subsingleton.elim _ _

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

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

Разделы

Аффилиация

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