copy_eq

Mathlib.Topology.CWComplex.Classical.Basic

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

← MathLib Explorer

English

If E.copy F hF J hJ is constructed with hF, hJ equalities to E, then it equals E.

Русский

Если копия копирования E.copy при равенствах hF, hJ с E, то она равна E.

LaTeX

$$$$E.copy F\, hF\, J\, hJ = E$$$$

Lean4

theorem copy_eq (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) → Set (cell C n)) (hJ : J = E.I) :
    E.copy F hF J hJ = E :=
  SetLike.coe_injective hF

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

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

Разделы

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

Аффилиация

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