ext

Mathlib.Topology.CWComplex.Classical.Basic

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

English

If two subcomplexes E and F have the same membership for all x ∈ X, then E = F.

Русский

Если два подкомплексa E и F имеют одинаковое членство для всех x ∈ X, то E = F.

LaTeX

$$$$\forall E,F : Subcomplex C,\; (\forall x, x \in E \iff x \in F) \Rightarrow E = F$$$$

Lean4

@[ext]
theorem ext {E F : Subcomplex C} (h : ∀ x, x ∈ E ↔ x ∈ F) : E = F :=
  SetLike.ext h

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

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

Разделы

Аффилиация

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