congr_apply_of — Mathlib

English

The congruence respects the application of component equivalences to elements in the direct limit.

Русский

Согласование сохраняет применение компонентных эквивалентностей к элементам прямого предела.

LaTeX

$$$e \\mapsto (f,g)\\;\\Rightarrow\\; (congr e he)(of i g) = of i (e i g).$$$

Lean4

theorem congr_apply_of (e : (i : ι) → G i ≃+* G' i)
    (he : ∀ i j h, (e j).toRingHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G i) :
    congr e he (of G _ i g) = of G' (fun _ _ h ↦ f' _ _ h) i (e i g) :=
  map_apply_of _ he _

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