of_f — Mathlib

English

There is an induction principle along a directed system: to prove a property C on the direct limit, it suffices to prove C on all components G_i via their injections.

Русский

Существует принцип индукции вдоль направленной системы: чтобы доказать свойство C на прямом пределе, достаточно доказать C на всех компонентах G_i через их внедрения.

LaTeX

$$$\forall z:\varinjlim G f,\; C(z) \equiv (\exists i,x:\; z=\iota_i(x) \land C\bigl(\iota_i(x)\bigr))$$$

Lean4

@[simp]
theorem of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x :=
  Module.DirectLimit.of_f

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