Structures · Analysis
DenselyNormedField
A densely normed field is a normed field for which the image of the norm is dense in ℝ≥0,
which means it is also nontrivially normed. However, not all nontrivially normed fields are densely
normed; in particular, the Padics exhibit this fact.
- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Shape
- One type argument · adds lt_norm_lt
Extends1
Extended by1
Forgetful instances
Every DenselyNormedField is also a
Concrete types that are instances3
- Real
- Rat
- Complex
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm
- ContinuousLinearMap.sSup_unit_ball_eq_nnnorm
- NormedField.exists_lt_nnnorm_lt
- ContinuousLinearMap.sSup_unitClosedBall_eq_norm
- ContinuousLinearMap.sSup_sphere_eq_nnnorm
- NormedField.exists_lt_norm_lt
- ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm
- ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm
- DenselyNormedField.lt_norm_lt
- ContinuousLinearMap.exists_lt_apply_of_lt_opNorm
- NormedField.denselyOrdered_range_norm
- DenselyNormedField.toNontriviallyNormedField
- DenselyNormedField.toNormedField
- DoubleCentralizer.instCStarRing
- NormedField.denseRange_nnnorm
- NormedField.denselyOrdered_range_nnnorm
- Unitization.norm_splitMul_snd_sq
- CStarRing.instRegularNormedAlgebra
- ContinuousLinearMap.sSup_unit_ball_eq_norm
- ContinuousLinearMap.sSup_sphere_eq_norm
- Unitization.instCStarRing
Ancestors157
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommGroupWithOne
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddGroup
- AddGroupWithOne
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddMonoidWithOne
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- AlgebraicGeometry.QuasiSeparated
- Bornology
- Bracket
- ChartedSpace
- CommGroupWithZero
- CommMagma
- CommMonoid
- CommMonoidWithZero
- CommRing
- CommSemigroup
- CommSemiring
- CompactSpace
- CompactlyCoherentSpace
- Dist
- Distrib
- Div
- DivInvMonoid
- DivInvOneMonoid
- DivisionCommMonoid
- DivisionMonoid
- DivisionRing
- DivisionSemiring
- Dvd
- EDist
- EMetricSpace
- ENorm
- EuclideanDomain
- Field
- GroupWithZero
- HAdd
- HDiv
- HMod
- HMul
- HSMul
- HSub
- HVAdd
- Ideal.FiniteHeight
- Infinite
- IntCast
- Inv
- InvOneClass
- InvolutiveInv
- InvolutiveNeg
- IsJacobsonRing
- IsLeftCancelAdd
- IsRightCancelAdd
- IsSemiprimaryRing
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.CommRing
- Lean.Grind.CommSemiring
- Lean.Grind.Field
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Lean.Grind.Ring
- Lean.Grind.Semiring
- LocallyPathConnectedSpace
- MetricSpace
- Mod
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NNDist
- NNNorm
- NNRatCast
- NPow
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocCommRing
- NonAssocCommSemiring
- NonAssocRing
- NonAssocSemiring
- NonUnitalCommRing
- NonUnitalCommSemiring
- NonUnitalNonAssocCommRing
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalNormedCommRing
- NonUnitalNormedRing
- NonUnitalRing
- NonUnitalSeminormedCommRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Nontrivial
- NontriviallyNormedField
- Norm
- NormedAddCommGroup
- NormedAddGroup
- NormedCommRing
- NormedDivisionRing
- NormedField
- NormedRing
- OfNat
- OfScientific
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- RatCast
- Ring
- SMul
- Semifield
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- SeminormedCommRing
- SeminormedRing
- Semiring
- SequentialSpace
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZPow
- ZSMul
- Zero