of_f — Mathlib

English

In the directed system of modules, the transition maps commute with the inclusions: the image of f i j hij x in G j, then included into the limit, equals the image of x included from G i.

Русский

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

LaTeX

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

Lean4

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

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