continuous_CC'₀

Mathlib.Topology.Category.Profinite.Nobeling.Successor

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

English

Continuity of CC'₀ with a refined proof step.

Русский

Непрерывность CC'₀ допущена на следующем шаге доказательства.

LaTeX

$$Continuous (CC'₀ C ho)$$

Lean4

theorem continuous_CC'₀ : Continuous (CC'₀ C ho) :=
  Continuous.subtype_mk continuous_subtype_val _

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

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

Разделы

Аффилиация

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