forall_isFixedPt_iff

Mathlib.Dynamics.FixedPoints.Basic

URI: https://scilib.ai/kg/mathlib#Function.forall_isFixedPt_iff

← MathLib Explorer

English

A function fixes every point if and only if it is the identity.

Русский

Функция фиксирует каждую точку тогда и только тогда, когда она тождественна.

LaTeX

$$$(\forall x, IsFixedPt f x) \iff f = \text{id}$$$

Lean4

/-- A function fixes every point iff it is the identity. -/
@[simp]
theorem forall_isFixedPt_iff : (∀ x, IsFixedPt f x) ↔ f = id :=
  ⟨funext, fun h ↦ h ▸ isFixedPt_id⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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