Theorems · Inductive type · field theory
DenselyNormedField
Type u_5 → Type u_5
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
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by25
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.exists_lt_apply_of_lt_opNNNormstatement and proof · cited by 3
- NormedField.exists_lt_nnnorm_ltstatement and proof · cited by 2
- ContinuousLinearMap.sSup_unit_ball_eq_nnnormstatement and proof · cited by 2
- DenselyNormedField.lt_norm_ltstatement and proof · cited by 1
- NormedField.exists_lt_norm_ltstatement and proof · cited by 1
- ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNormstatement and proof · cited by 1
- ContinuousLinearMap.sSup_sphere_eq_nnnormstatement and proof · cited by 1
- ContinuousLinearMap.sSup_unitClosedBall_eq_nnnormstatement and proof · cited by 1
- ContinuousLinearMap.sSup_unitClosedBall_eq_normstatement and proof · cited by 1
- DenselyNormedField.casesOnstatement and proof · cited by 0
- DenselyNormedField.ctorIdxstatement and proof · cited by 0
- DenselyNormedField.noConfusionstatement and proof · cited by 0