subset_complex — Mathlib

English

For any subcomplex E, the underlying set ↑E is contained in C.

Русский

Для любого подкомплексa E множество ↑E содержится в C.

LaTeX

$$$$\\uparrow E \\subseteq C$$$$

Lean4

theorem subset_complex {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) : ↑E ⊆ C :=
  by
  simp_rw [← union, ← RelCWComplex.union_iUnion_openCell_eq_complex]
  exact union_subset_union_right _ (iUnion_mono fun _ ↦ iUnion_mono' fun j ↦ ⟨j, subset_rfl⟩)

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