English
Let (C, D) be a RelCWComplex. For any n ∈ ENat and x ∈ X, x ∈ skeleton C n if and only if x ∈ D or there exists m ≤ n and j ∈ cell C m with x ∈ openCell(m, j).
Русский
Пусть (C, D) — относительный CW-комплекс. Для любого n ∈ ENat и точки x: x ∈ skeleton(C, n) тогда и только тогда, когда x ∈ D или существует m ≤ n и j ∈ cell(C, m) такие, что x ∈ openCell(m, j).
LaTeX
$$$$ x \\in skeleton(C,n) \\iff x \\in D \\lor \\exists m \\in \\mathbb{N},\\; m \\le n \\land \\exists j \\in cell(C,m),\\; x \\in openCell(m,j). $$$$
Lean4
theorem mem_skeleton_iff [RelCWComplex C D] {n : ℕ∞} {x : X} :
x ∈ skeleton C n ↔ x ∈ D ∨ ∃ (m : ℕ) (_ : m ≤ n) (j : cell C m), x ∈ openCell m j :=
by
rw [skeleton, mem_skeletonLT_iff]
suffices ∀ (m : ℕ), m < n + 1 ↔ m ≤ n by simp_rw [this]
intro m
cases n
· simp
· rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_iff]
