isIndObject_inclusion_obj — Mathlib

English

The inclusion of C into Ind(C) sends any Ind-object X to an Ind-object; more precisely, the inclusion preserves the Ind-structure.

Русский

Включение C в Ind(C) переводит любой Ind-объект X в Ind-объект; точнее, включение сохраняет структуру Ind.

LaTeX

$$$((\mathrm{Ind.inclusion}\,C).\mathrm{obj}\,X) \text{ is an Ind-object}$$$

Lean4

theorem isIndObject_inclusion_obj (X : Ind C) : IsIndObject ((Ind.inclusion C).obj X) :=
  X.2

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