Structures · Analysis
NNNorm
Auxiliary class, endowing a type α with a function nnnorm : α → ℝ≥0 with notation ‖x‖₊.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds nnnorm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Concrete types that are instances7
- Quiver.Hom
- NNReal
- Subtype
- OrderDual
- ULift
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by36
- NNNorm.nnnorm
- enorm_ne_top
- enorm_eq_nnnorm
- egauge_le_of_mem_smul
- egauge_anti
- Set.MapsTo.egauge_le
- enorm_le_coe
- le_egauge_iff
- egauge_lt_iff
- le_egauge_prod
- le_egauge_pi
- coe_le_enorm
- egauge_zero_left_eq_top
- enorm_lt_coe
- enorm_lt_top
- nnnorm_ofDual
- NNNorm.toENorm
- nnnorm_ofAdd
- nnnorm_toDual
- OrderDual.toNNNorm
- ULift.nnnorm_def
- ULift.nnnorm_up
- Multiplicative.toNNNorm
- Additive.toNNNorm
- nnnorm_toAdd
- toNNReal_enorm
- le_egauge_inter
- nnnorm_ofMul
- coe_lt_enorm
- egauge_union
- egauge_empty
- egauge_eq_top
- nnnorm_toMul
- egauge_zero_left
- ULift.nnnorm
- ULift.nnnorm_down