of_f

Mathlib.Algebra.Colimit.Ring

URI: https://scilib.ai/kg/mathlib#Ring.DirectLimit.of_f

English

There exists i and x such that z = of G f i x for any z in Ring.DirectLimit G f.

Русский

Существует i и x such that z equals the embedding of x from G_i into the direct limit.

LaTeX

$$$\exists i\;\exists x:\; of G f i x = z$$$

Lean4

@[simp]
theorem of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x :=
  Ideal.Quotient.eq.2 <| subset_span <| Or.inl ⟨i, j, hij, x, rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru