CC'₁

Mathlib.Topology.Category.Profinite.Nobeling.Successor

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.CC'₁

← MathLib Explorer

English

Equivalence between CC'₀ on g and a certain elementary expression.

Русский

Эквивалентность между CC'₀ на g и определенным элементарным выражением.

LaTeX

$$Eq (Profinite.NobelingProof.CC'₀ C ho g) ⟨g.val, ⋯⟩$$

Lean4

/-- The second way to map `C'` into `C`. -/
noncomputable def CC'₁ : C' C ho → C := fun g ↦ ⟨SwapTrue o g.val, (swapTrue_mem_C1 C hsC ho ⟨g.val, g.prop.2⟩).1⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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