map_apply_of — Mathlib

English

Given compatible families g_i and f-bonds, the map induced by g on the direct limit sends the canonical image of x ∈ G_i to the image g_i(x) in G'_i.

Русский

Дано систему совместимых отображений и отображения связывания, отображение, индуцированное отображением g на прямой предел, отправляет каноническое образ G_i в g_i(x).

LaTeX

$$$\\mathrm{map}\\;g\\;hg\\; (\\mathrm{of}\\;G\\;f\\;i\\;x) = \\mathrm{of}\\;G'\\; (f')\\;i\\; (g_i(x)).$$$

Lean4

@[simp]
theorem map_apply_of (g : (i : ι) → G i →+* G' i) (hg : ∀ i j h, (g j).comp (f i j h) = (f' i j h).comp (g i)) {i : ι}
    (x : G i) : map g hg (of G _ _ x) = of G' (fun _ _ h ↦ f' _ _ h) i (g i x) :=
  lift_of _ _ _ _ _

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