eq_iff

Mathlib.Topology.CWComplex.Classical.Basic

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

English

Equality of subcomplexes E = F is equivalent to equality of their coerced carriers.

Русский

Равенство подкомплексoв E = F эквивалентно равенству их носителей (коэрцированные множества).

LaTeX

$$$$E = F \;\Leftrightarrow\; (E : Set X) = F$$$$

Lean4

theorem eq_iff (E F : Subcomplex C) : E = F ↔ (E : Set X) = F :=
  SetLike.coe_injective.eq_iff.symm

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

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

Разделы

Аффилиация

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