rangeLiftInclusion

Mathlib.ModelTheory.DirectLimit

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.DirectLimit.rangeLiftInclusion

English

The direct limit is countably generated under suitable hypotheses (restatement).

Русский

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

LaTeX

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

Lean4

theorem rangeLiftInclusion : (liftInclusion S).toHom.range = ⨆ i, S i := by
  simp_rw [liftInclusion, range_lift, Substructure.range_subtype]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru