cg' — Mathlib

English

The directed limit of countably generated structures is countably generated.

Русский

Предел направленной системы счетно порожденных структур счетно порожден.

LaTeX

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

Lean4

instance cg' {ι : Type*} [Countable ι] [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι] {G : ι → Type w}
    [∀ i, L.Structure (G i)] (f : ∀ i j, i ≤ j → G i ↪[L] G j) [h : ∀ i, Structure.CG L (G i)]
    [DirectedSystem G fun i j h => f i j h] : Structure.CG L (DirectLimit G f) :=
  cg f h

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