map_map' — Mathlib

English

A direct limit admits an induction principle: to prove a property for every element, it suffices to prove it for representatives.

Русский

Прямой предел обладает принципом индукции: достаточно доказать свойство для представителя каждого элемента.

LaTeX

$$$\text{DirectLimit.induction}: \forall C:\ DirectLimit F f \to Prop, (\forall i x, C (⟦⟨i,x⟩⟧)) \Rightarrow \forall z, C z.$$$

Lean4

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

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