Mathlib Map

Theorems · Theorem · functional analysis

nnnorm_surjective

∀ (E : Type u_1) [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E], Function.Surjective nnnorm
Defined in
Mathlib.Analysis.Normed.Module.RCLike.Real
Cited by
1 results in Mathlib
Foundations
Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SeminormedAddCommGroupNormedSpaceNontrivialTopology
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

range_nnnorm · cited by 0range_nnnormReal · cited by 25697RealNormedSpace · cited by 12499NormedSpaceNNReal · cited by 4310NNRealSeminormedAddCommGroup · cited by 2671SeminormedAddCommGroupNNReal.toReal · cited by 1260NNReal.toRealNNNorm.nnnorm · cited by 952NNNorm.nnnormNNReal.eq · cited by 201NNReal.eqNNReal.coe_nonneg · cited by 130NNReal.coe_nonnegNontrivialTopology · cited by 46NontrivialTopologyexists_norm_eq · cited by 4exists_norm_eqnnnorm_surjectiveCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.