basicCell — Mathlib

English

For each n, there is a canonical morphism ∂𝔻_n → 𝔻_n, given by diskBoundaryInclusion n.

Русский

Для каждого n существует каноническое отображение ∂𝔻_n → 𝔻_n, задаваемое diskBoundaryInclusion n.

LaTeX

$$$BasicCell(n) = diskBoundaryInclusion(n)$$$

Lean4

/-- For each `n : ℕ`, this is the family of morphisms which sends the unique
element of `Unit` to `diskBoundaryInclusion n : ∂𝔻 n ⟶ 𝔻 n`. -/
@[nolint unusedArguments]
abbrev basicCell (n : ℕ) (_ : Unit) : ∂𝔻 n ⟶ 𝔻 n :=
  diskBoundaryInclusion n

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