toCWComplex_eq

Mathlib.Topology.CWComplex.Classical.Basic

URI: https://scilib.ai/kg/mathlib#Topology.RelCWComplex.toCWComplex_eq

English

The RelCWComplex instance extracted from toCWComplex equals the original one.

Русский

Экземпляр RelCWComplex, получаемый из toCWComplex, равен исходному.

LaTeX

$$$(Topology.RelCWComplex.toCWComplex\, C).instRelCWComplex = h$$$

Lean4

theorem toCWComplex_eq {X : Type*} [TopologicalSpace X] (C : Set X) [h : RelCWComplex C ∅] :
    (toCWComplex C).instRelCWComplex = h :=
  rfl

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

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

Разделы

Аффилиация

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