openCell — Mathlib

English

The open n-cell is defined as the image of ball 0 1 under the map of i.

Русский

Открытая n-клетка задаётся как образ сферыball 0 1 под отображением i.

LaTeX

$$$openCell\; (n)\; (i) = map\; n\; i \\"'\text{ball } 0 1}$$$

Lean4

/-- The open `n`-cell given by the index `i`. Use this instead of `map n i '' ball 0 1` whenever
possible. -/
def openCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set X :=
  map n i '' ball 0 1

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