of_f — Mathlib

English

In the ring setting, the canonical inclusions satisfy the same compatibility: the image of f i j hij x in G_j, when mapped to the limit via the jth inclusion, equals the image from i via the i-th inclusion.

Русский

В кольцевом случае образ f i j hij x в G_j, затем отображённый через инклюзию в предел, равен образу x из G_i, включённому в предел.

LaTeX

$$$\\text{of}(j, f(i,j,h)x) = \\text{of}(i, x).$$$

Lean4

@[simp]
theorem of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x :=
  .symm <| eq_of_le ..

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