mem_skeletonLT_iff — Mathlib

English

Let (C, D) be a RelCWComplex. For any n ∈ ENat and x in X, x lies in skeletonLT(C, n) precisely when x ∈ D or there exists m < n and a cell j ∈ cell(C, m) with x ∈ openCell(m, j).

Русский

Пусть (C, D) — относительный CW-комплекс. Тогда для любого n ∈ ENat и точки x: x ∈ skeletonLT(C, n) тогда и только тогда, когда x ∈ D или существует m < n и.cell j ∈ cell(C, m), такое что x ∈ openCell(m, j).

LaTeX

$$$$ x \\in skeletonLT(C,n) \\iff x \\in D \\lor \\exists m \\in \\mathbb{N},\\; m < n \\land \\exists j \\in cell(C,m),\\; x \\in openCell(m,j). $$$$

Lean4

theorem mem_skeletonLT_iff [RelCWComplex C D] {n : ℕ∞} {x : X} :
    x ∈ skeletonLT C n ↔ x ∈ D ∨ ∃ (m : ℕ) (_ : m < n) (j : cell C m), x ∈ openCell m j := by
  simp [← SetLike.mem_coe, ← iUnion_openCell_eq_skeletonLT]

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