contained_C1

Mathlib.Topology.Category.Profinite.Nobeling.Successor

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.contained_C1

English

The projection of C' is contained at level o.

Русский

Проекция C' ограничена на уровне o.

LaTeX

$$contained (C' C ho) o$$

Lean4

theorem contained_C1 : contained (π (C1 C ho) (ord I · < o)) o :=
  contained_proj _ _

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

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

Разделы

Аффилиация

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