cellFrontier_subset_base_union_finite_closedCell

English

The frontier is contained in the base union with a finite collection of closed cells.

Русский

Граница подмножество объединения основы с конечной коллекцией замкнутых клеток.

LaTeX

$$$cellFrontier n i ⊆ D ∪ ⋃ (m < n) (j ∈ I m), closedCell m j$ для некоторого семейства I.$$

Lean4

theorem cellFrontier_subset_base_union_finite_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) :
    ∃ I : Π m, Finset (cell C m), cellFrontier n i ⊆ D ∪ ⋃ (m < n) (j ∈ I m), closedCell m j :=
  by
  rcases mapsTo n i with ⟨I, hI⟩
  use I
  rw [mapsTo_iff_image_subset] at hI
  exact hI

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