cellFrontier_subset_skeletonLT — Mathlib

English

For RelCWComplex C D and j ∈ cell C n, the cellFrontier n j is contained in skeletonLT C n.

Русский

Для RelCWComplex C D и j∈cell C n frontier клетки cellFrontier n j ⊆ skeletonLT C n.

LaTeX

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

Lean4

theorem cellFrontier_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) : cellFrontier n j ⊆ skeletonLT C n :=
  by
  obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell n j
  apply subset_trans hI
  rw [coe_skeletonLT]
  apply union_subset_union_right
  intro x xmem
  simp only [mem_iUnion, exists_prop] at xmem ⊢
  obtain ⟨i, iltn, j, _, xmem⟩ := xmem
  exact ⟨i, by norm_cast, j, xmem⟩

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