iUnion_skeletonLT_eq_complex — Mathlib

English

Equivalent formulation asserting the union of skeletonLT over n recovers C.

Русский

Альтернативная формулировка: объединение skeletonLT по n возвращает C.

LaTeX

$$$\\bigcup_{n\\in\\mathbb{N}}\\mathrm{skeletonLT}(C,D;n)=C$$$

Lean4

theorem iUnion_skeletonLT_eq_complex [RelCWComplex C D] : ⋃ (n : ℕ), skeletonLT C n = C :=
  by
  apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeletonLT C _).subset_complex)
  simp_rw [← union_iUnion_openCell_eq_complex, union_subset_iff, iUnion₂_subset_iff]
  exact
    ⟨subset_iUnion_of_subset 0 (skeletonLT C 0).base_subset, fun n i ↦
      subset_iUnion_of_subset _ (openCell_subset_skeletonLT n i)⟩

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