instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion

English

A variant of CG for the direct limit, showing that the direct limit inherits the CG property from the system.

Русский

Вариант CG для прямого предела, показывающий, что предел наследует свойство CG от системы.

LaTeX

$$$\text{cg}\; f\; h.$$$

Lean4

instance : DirectedSystem (fun i ↦ S i) (fun _ _ h ↦ Substructure.inclusion (S.monotone h))
    where
  map_self _ _ := rfl
  map_map _ _ _ _ _ _ := rfl

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