map_self' — Mathlib

English

Within a directed system with FunLike structure, the map from F(i) to F(i) along identity is the identity.

Русский

В направленной системе с структурой FunLike отображение F(i) → F(i) по тождению является тождественным.

LaTeX

$$$\forall i\, x, f\_i^i\ le_rfl (x) = x$ where $f$ is the directed system map.$$

Lean4

/-- A copy of `DirectedSystem.map_self` specialized to FunLike, as otherwise the
`fun i j h ↦ f i j h` can confuse the simplifier. -/
theorem map_self' ⦃i⦄ (x) : f i i le_rfl x = x :=
  DirectedSystem.map_self (f := (f · · ·)) x

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