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	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule 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	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 ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup Top.top instTopENNReal	—	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