Documentation

LeanPool.WhiteheadTheorem.Shapes.Disk

LeanPool.WhiteheadTheorem.Shapes.Disk #

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Shapes.Disk.

source
def TopCat.diskBoundaryIncl (n : ℕ) :
diskBoundary n ⟶ disk n

The inclusion ∂𝔻 n ⟶ 𝔻 n of the boundary of the n-disk.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance TopCat.isEmpty_diskBoundary_zero :
    IsEmpty ↑(diskBoundary 0)