Documentation

LeanPool.OneManifold.OneMfld.UnitInterval

UnitInterval #

Supporting results for the classification of compact one-dimensional manifolds.

source
@[reducible, inline]
abbrev OneMfld.UnitInterval :
Set ℝ

The closed unit interval in the real line.

Equations
Instances For
    source
    theorem OneMfld.UnitInterval_eq_Icc :
    UnitInterval = Set.Icc 0 1

    UnitInterval is definitionally Set.Icc 0 1; this bridge unlocks Mathlib's Icc API (e.g. iccHomeoI, isCompact_Icc) for it.

    source
    theorem OneMfld.isCompact_UnitInterval :
    IsCompact UnitInterval