Theorems · Theorem · functional analysis
norm_withSeminorms
∀ (𝕜 : Type u_11) (E : Type u_12) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], WithSeminorms fun x => normSeminorm 𝕜 E
The topology of a NormedSpace 𝕜 E is induced by the seminorm normSeminorm 𝕜 E.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- NormedSpacestatement and proof · cited by 12,499
- Filterproof · cited by 8,121
- nhdsproof · cited by 5,554
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- NormedFieldstatement and proof · cited by 1,084
- Filter.comapproof · cited by 546
- WithSeminormsstatement · cited by 69
- normSeminormstatement and proof · cited by 32
- iInf_constproof · cited by 9
- SeminormFamily.withSeminorms_iff_nhds_eq_iInfproof · cited by 8
- comap_norm_nhds_zeroproof · cited by 7
Cited by12
Results whose statement or proof uses this declaration.
- WithSeminorms.continuous_normedSpace_rngproof · cited by 4
- banach_steinhausproof · cited by 3
- LinearMap.weakBilin_withSeminormsproof · cited by 2
- NormedSpace.equicontinuous_TFAEproof · cited by 2
- PointwiseConvergenceCLM.withSeminormsproof · cited by 2
- LinearMap.mem_span_iff_continuousproof · cited by 1
- ContinuousLinearMapWOT.withSeminormsproof · cited by 1
- ContDiffMapSupportedIn.withSeminormsproof · cited by 1
- WithSeminorms.continuous_normedSpace_domproof · cited by 1
- banach_steinhaus_iSup_nnnormproof · cited by 0
- NormedSpace.toLocallyConvexSpace'proof · cited by 0
- LinearMap.mem_span_iff_boundproof · cited by 0