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