closedCell_subset_skeletonLT — Mathlib

English

For any RelCWComplex C D, n ∈ ℕ and j ∈ cell C n, the closed cell closedCell n j is contained in skeletonLT C (n+1).

Русский

Для любого RelCWComplex C D, натурального n и клетки j∈cell C n, замкнутая клетка closedCell n j содержится в skeletonLT C (n+1).

LaTeX

$$$\\text{closedCell}(n,j)\\subseteq \\mathrm{skeletonLT}(C,D;n+1)$$$

Lean4

theorem closedCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) :
    closedCell n j ⊆ skeletonLT C (n + 1) := by
  intro x xmem
  rw [coe_skeletonLT]
  right
  simp_rw [mem_iUnion, exists_prop]
  refine ⟨n, (by norm_cast; exact lt_add_one n), ⟨j, xmem⟩⟩

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