Documentation Verification Report

Barrelled

📁 Source: Mathlib/Analysis/LocallyConvex/Barrelled.lean

Statistics

Metric	Count
Definitions `BarrelledSpace`, `continuousLinearMapOfTendsto`, `continuousLinearMapOfTendsto`	3
Theorems `instBarrelledSpace`, `continuous_of_lowerSemicontinuous`, `banach_steinhaus`, `continuous_iSup`, `continuous_of_lowerSemicontinuous`, `banach_steinhaus`	6
Total	9

BaireSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instBarrelledSpace` 📖	mathematical	—	`BarrelledSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`Seminorm.closedBall_zero_eq` `LowerSemicontinuous.isClosed_preimage` `Set.eq_univ_of_forall` `Set.mem_iUnion` `exists_nat_ge` `Real.instIsOrderedRing` `Real.instArchimedean` `nonempty_interior_of_iUnion_of_closed` `AddTorsor.nonempty` `instCountableNat` `Seminorm.continuous'` `interior_subset` `Filter.mp_mem` `map_add_left_nhds_zero` `mem_interior_iff_mem_nhds` `Filter.univ_mem'` `add_sub_cancel_left` `map_sub_le_add` `SeminormClass.toAddGroupSeminormClass` `Seminorm.instSeminormClass` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`

BarrelledSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_of_lowerSemicontinuous` 📖	mathematical	`LowerSemicontinuous` `Real` `Real.instPreorder` `DFunLike.coe` `Seminorm` `Seminorm.instFunLike`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	—

PolynormableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`banach_steinhaus` 📖	mathematical	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformSpace.toTopologicalSpace` `Set.range` `DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	`UniformEquicontinuous`	—	`withSeminorms` `WithSeminorms.banach_steinhaus` `WithSeminorms.isVonNBounded_iff_seminorm_bddAbove`

Seminorm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_iSup` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DFunLike.coe` `Seminorm` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `AddCommGroup.toAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `instFunLike` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set.range`	`iSup` `Pi.supSet` `Real.instSupSet`	—	`coe_iSup_eq` `continuous_of_lowerSemicontinuous` `iSup_apply` `lowerSemicontinuous_ciSup` `bddAbove_range_iff` `Continuous.lowerSemicontinuous` `instOrderTopologyReal`
`continuous_of_lowerSemicontinuous` 📖	mathematical	`LowerSemicontinuous` `Real` `Real.instPreorder` `DFunLike.coe` `Seminorm` `instFunLike`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`BarrelledSpace.continuous_of_lowerSemicontinuous`

WithSeminorms

Definitions

Name	Category	Theorems
`continuousLinearMapOfTendsto` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`banach_steinhaus` 📖	mathematical	`WithSeminorms` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `BddAbove` `Real` `Real.instLE` `Set.range` `DFunLike.coe` `Seminorm` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `AddCommGroup.toAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Seminorm.instFunLike` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ContinuousLinearMap.funLike`	`UniformEquicontinuous`	—	`uniformEquicontinuous_iff_bddAbove_and_continuous_iSup` `Seminorm.bddAbove_range_iff` `Seminorm.continuous_iSup` `Continuous.comp` `continuous_seminorm` `ContinuousLinearMap.continuous`

(root)

Definitions

Name	Category	Theorems
`BarrelledSpace` 📖	CompData	1 math math: `BaireSpace.instBarrelledSpace`
`continuousLinearMapOfTendsto` 📖	CompOp	—

---

← Back to Index