contained_C'

Mathlib.Topology.Category.Profinite.Nobeling.Successor

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

English

Equality of Linear_CC'₀ and Linear_CC'₁ under specific arguments.

Русский

Равенство Linear_CC'₀ и Linear_CC'₁ при соответствующих аргументах.

LaTeX

$$Eq (Profinite.NobelingProof.Linear_CC' C ho) (Profinite.NobelingProof.Linear_CC'₁ C hsC ho)$$

Lean4

theorem contained_C' : contained (C' C ho) o := fun f hf i hi ↦ contained_C1 C ho f hf.2 i hi

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

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

Разделы

Аффилиация

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