Theorems · Theorem · functional analysis
WithSeminorms.continuous_normedSpace_rng
∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {ι : Type u_9} [inst : AddCommGroup E] [inst_1 : NormedField 𝕝]
[inst_2 : Module 𝕝 E] [inst_3 : NormedField 𝕝₂] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_4 : RingHomIsometric τ₁₂] (F : Type u_11)
[inst_5 : SeminormedAddCommGroup F] [inst_6 : NormedSpace 𝕝₂ F] [inst_7 : TopologicalSpace E] {p : ι → Seminorm 𝕝 E},
WithSeminorms p → ∀ (f : E →ₛₗ[τ₁₂] F), (∃ s C, (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) → Continuous ⇑f- Cited by
- 4 results in Mathlib
- Foundations
- Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Realstatement · cited by 25,697
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- Finsetstatement and proof · cited by 13,712
- AddCommGroupstatement and proof · cited by 12,871
- NormedSpacestatement and proof · cited by 12,499
- LinearMapstatement and proof · cited by 10,215
- RingHomstatement and proof · cited by 10,189
- NNRealstatement and proof · cited by 4,310
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- Continuousstatement · cited by 2,592
Cited by4
Results whose statement or proof uses this declaration.
- Module.Dual.exists_continuous_extension_of_le_seminormproof · cited by 2
- WithSeminorms.continuous_real_rngproof · cited by 1
- Seminorm.cont_withSeminorms_normedSpaceproof · cited by 0
- LinearMap.mem_span_iff_boundproof · cited by 0