exists_mem_openCell_of_mem_skeleton

English

For a CW complex (C, D) and any n ∈ ENat, x ∈ skeleton C n holds if and only if there exists m ≤ n and j ∈ cell C m with x ∈ openCell m j.

Русский

Пусть CW-комплекс (C, D) тогда x ∈ skeleton(C, n) эквивалентно существованию m ≤ n и j ∈ cell(C, m), такого что x ∈ openCell(m, j).

LaTeX

$$$$ x \\in skeleton(C,n) \\iff \\exists m \\le n,\\; \\exists j \\in cell(C,m),\\; x \\in openCell(m,j). $$$$

Lean4

theorem exists_mem_openCell_of_mem_skeleton [CWComplex C] {n : ℕ∞} {x : X} :
    x ∈ skeleton C n ↔ ∃ (m : ℕ) (_ : m ≤ n) (j : cell C m), x ∈ openCell m j := by
  rw [RelCWComplex.mem_skeleton_iff, mem_empty_iff_false, false_or]

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