CC'₀

Mathlib.Topology.Category.Profinite.Nobeling.Successor

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

English

The composed Linear_CC' map sends a πs y to zero.

Русский

Составной линейный отображение Linear_CC' отправляет πs y в ноль.

LaTeX

$$$ CC\_comp\_zero : \forall y, (Linear\_CC' C hsC ho) ((\pi s C o) y) = 0 $$$

Lean4

/-- The first way to map `C'` into `C`. -/
def CC'₀ : C' C ho → C := fun g ↦ ⟨g.val, g.prop.1.1⟩

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

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

Разделы

Аффилиация

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