base_subset_complex

Mathlib.Topology.CWComplex.Classical.Basic

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

English

D is a subset of C for RelCWComplex C D.

Русский

D ⊆ C для RelCWComplex C D.

LaTeX

$$$D \subseteq C$$$

Lean4

theorem base_subset_complex [RelCWComplex C D] : D ⊆ C :=
  by
  simp_rw [← union]
  exact subset_union_left

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

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

Разделы

Аффилиация

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