congr_apply_of — Mathlib

English

The map on direct limits respects the application of g to x from i via the direct limit's lift and inclusions.

Русский

Отображение на пределы соблюдает применение g к x из i через взвод предела и вложения.

LaTeX

$$$\\text{map\_apply\_of}(g,hg)(\\text{of}(i,x)) = \\text{of'}(i, g_i x)$$$

Lean4

theorem congr_apply_of (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ i j h, e j ∘ₗ f i j h = f' i j h ∘ₗ e i) {i : ι}
    (g : G i) : congr e he (of _ _ G f i g) = of _ _ G' f' i (e i g) :=
  map_apply_of _ he _

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