equiv_lift_of — Mathlib

English

If each G_i is countably generated in the language L, and the system is directed, then the direct limit is countably generated.

Русский

Если каждая G_i счетно порождена в языке L и система направлена, тогда прямой предел счетно порожден.

LaTeX

$$$\text{cg}\; L\; (DirectLimit G f).$$$

Lean4

theorem equiv_lift_of {i : ι} (x : G i) :
    equiv_lift L ι G f G' f' g H_commuting (of L ι G f i x) = of L ι G' f' i (g i x) :=
  rfl

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