mem_carrier

Mathlib.Topology.CWComplex.Classical.Basic

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

English

For a subcomplex E and x ∈ X, x ∈ E.carrier if and only if x ∈ E when viewed as a subset of X.

Русский

Для подкомплексa E и элемента x ∈ X верно: x ∈ E.carrier тогда и только тогда, когда x ∈ E как подмножество X.

LaTeX

$$$$x \in E.carrier \iff x \in (E : Set X)$$$$

Lean4

theorem mem_carrier {E : Subcomplex C} {x : X} : x ∈ E.carrier ↔ x ∈ (E : Set X) :=
  Iff.rfl

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

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

Разделы

Аффилиация

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