BanachSteinhaus

📁 Source: Mathlib/Analysis/Normed/Operator/BanachSteinhaus.lean

Statistics

Metric	Count
Definitions	0
Theorems banach_steinhaus, banach_steinhaus_iSup_nnnorm	2
Total	2

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
banach_steinhaus 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike	ContinuousLinearMap.hasOpNorm	—	List.TFAE.out NormedSpace.equicontinuous_TFAE WithSeminorms.banach_steinhaus SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul BaireSpace.instBarrelledSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul BaireSpace.of_completelyPseudoMetrizable TopologicalSpace.IsCompletelyPseudoMetrizableSpace.of_completeSpace_pseudometrizable EMetric.instIsCountablyGeneratedUniformity norm_withSeminorms
banach_steinhaus_iSup_nnnorm 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike Top.top instTopENNReal	ContinuousLinearMap.toSeminormedAddCommGroup	—	List.TFAE.out NormedSpace.equicontinuous_TFAE WithSeminorms.banach_steinhaus SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul BaireSpace.instBarrelledSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul BaireSpace.of_completelyPseudoMetrizable TopologicalSpace.IsCompletelyPseudoMetrizableSpace.of_completeSpace_pseudometrizable EMetric.instIsCountablyGeneratedUniformity norm_withSeminorms ENNReal.iSup_coe_lt_top

---

← Back to Index