Structures · Geometry
ENat.LEInfty
A typeclass registering that a smoothness exponent is smaller than ∞. Used to deduce that
some manifolds are C^n when they are C^∞.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- OfNat.ofNat
- WithTop.some
- Nat.cast
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- instContMDiffAddOfSomeENatTopOfLEInfty
- ENat.LEInfty.out
- IsManifold.instOfSomeENatTopOfLEInfty
- instContMDiffInv₀OfSomeENatTopOfLEInfty
- instContMDiffMulOfSomeENatTopOfLEInfty
- instContMDiffSMulOfSomeENatTopOfLEInfty
- instLieAddGroupOfSomeENatTopOfLEInfty
- instLieGroupOfSomeENatTopOfLEInfty
- instContMDiffVAddOfSomeENatTopOfLEInfty
- instContMDiffVectorBundleOfSomeENatTopOfLEInfty
- instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty
Ancestors0
No ancestors.