coe_eq_carrier

Mathlib.Topology.CWComplex.Classical.Basic

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

English

For a subcomplex E, the coerced set (E : Set X) equals E.carrier.

Русский

Для подкомплексa E приведённое к множеству множество (E : Set X) равно E.carrier.

LaTeX

$$$$(E : Set X) = E.carrier$$$$

Lean4

theorem coe_eq_carrier {E : Subcomplex C} : (E : Set X) = E.carrier :=
  rfl

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

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

Разделы

Аффилиация

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