map_apply_of — Mathlib

English

A compatibly defined map from a directed system to a target commutes with the canonical inclusions when applied to an element from a component.

Русский

Совместимо определённое отображение между системами и целевым модулем commute с каноническими включениями на элементе из компоненты.

LaTeX

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

Lean4

@[simp]
theorem map_apply_of (g : (i : ι) → G i →ₗ[R] G' i) (hg : ∀ i j h, g j ∘ₗ f i j h = f' i j h ∘ₗ g i) {i : ι} (x : G i) :
    map g hg (of _ _ G f _ x) = of R ι G' f' i (g i x) :=
  lift_of _ _ _

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