map_zero_mem_openCell — Mathlib

English

In a RelCWComplex, the base point of the nth cell i lies in the corresponding open cell: (map n i).toFun 0 ∈ openCell n i.

Русский

В RelCWComplex базовая точка клетки n i принадлежит соответствующей открытой клетке: (map n i).toFun 0 ∈ openCell n i.

LaTeX

$$$((\mathrm{map}\ n\ i).toFun\ 0) \in openCell\ n\ i$$$

Lean4

theorem map_zero_mem_openCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : map n i 0 ∈ openCell n i :=
  by
  apply mem_image_of_mem
  simp only [mem_ball, dist_self, zero_lt_one]

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