Documentation Verification Report

WeakDual

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

Statistics

Metric	Count
Definitions `toSeminorm`, `toSeminormFamily`	2
Theorems `coe_toSeminorm`, `hasBasis_weakBilin`, `mem_span_iff_bound`, `mem_span_iff_continuous`, `mem_span_iff_continuous_of_finite`, `toSeminormFamily_apply`, `toSeminorm_apply`, `toSeminorm_ball_zero`, `toSeminorm_comp`, `weakBilin_withSeminorms`, `locallyConvexSpace`	11
Total	13

LinearMap

Definitions

Name	Category	Theorems
`toSeminorm` 📖	CompOp	5 math math: `coe_toSeminorm`, `toSeminorm_comp`, `toSeminorm_ball_zero`, `toSeminorm_apply`, `mem_span_iff_bound`
`toSeminormFamily` 📖	CompOp	3 math math: `hasBasis_weakBilin`, `weakBilin_withSeminorms`, `toSeminormFamily_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toSeminorm` 📖	mathematical	—	`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` `Real` `Seminorm.instFunLike` `toSeminorm` `Norm.norm` `NormedField.toNorm` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `instFunLike`	—	—
`hasBasis_weakBilin` 📖	mathematical	—	`Filter.HasBasis` `WeakBilin` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `AddCommGroup.toAddCommMonoid` `Set` `nhds` `WeakBilin.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WeakBilin.instAddCommGroup` `SeminormFamily.basisSets` `toSeminormFamily`	—	`Algebra.to_smulCommClass` `WithSeminorms.hasBasis` `weakBilin_withSeminorms`
`mem_span_iff_bound` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Submodule` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Seminorm` `AddCommGroup.toAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `Seminorm.instPartialOrder` `toSeminorm` `NNReal` `Seminorm.instSMul` `Algebra.toSMul` `Real` `instCommSemiringNNReal` `Real.semiring` `NNReal.instAlgebraOfReal` `Real.instCommSemiring` `IsScalarTower.left` `instSemiringNNReal` `NNReal.instMulActionOfReal` `DistribMulAction.toMulAction` `Real.instMonoid` `AddCommMonoid.toAddMonoid` `Real.instAddCommMonoid` `Real.normedField` `Real.normedCommRing` `Finset.sup` `Seminorm.instSemilatticeSup` `Seminorm.instOrderBot`	—	`topologicalAddGroup_iInf` `topologicalAddGroup_induced` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `nhds_iInf` `nhds_induced` `map_zero` `AddMonoidHomClass.toZeroHomClass` `comap_norm_nhds_zero` `Filter.comap_comap` `Algebra.to_smulCommClass` `IsScalarTower.left` `mem_span_iff_continuous` `RingHomIsometric.ids` `Seminorm.bound_of_continuous` `Seminorm.continuous_iff_continuous_comp` `norm_withSeminorms` `Seminorm.cont_withSeminorms_normedSpace`
`mem_span_iff_continuous` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Submodule` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Continuous` `iInf` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.induced` `DFunLike.coe` `instFunLike`	—	`topologicalAddGroup_iInf` `topologicalAddGroup_induced` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `continuousSMul_iInf` `continuousSMul_induced` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SemilinearMapClass.toMulActionSemiHomClass` `RingHomIsometric.ids` `Seminorm.continuous_iff_continuous_comp` `norm_withSeminorms` `Seminorm.continuous_iff` `ContinuousSMul.continuousConstSMul` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `nhds_iInf` `iInf_subtype` `Filter.mem_iInf_finite` `Algebra.to_smulCommClass` `Finite.of_fintype` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `Submodule.span_range_eq_iSup` `iSup_subtype` `iSup_congr_Prop` `Submodule.mem_iSup_iff_exists_finset`
`mem_span_iff_continuous_of_finite` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `Submodule` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Continuous` `iInf` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.induced` `DFunLike.coe` `instFunLike`	—	`Algebra.to_smulCommClass` `Submodule.span_induction` `Set.forall_mem_range` `continuous_iInf_dom` `continuous_induced_dom` `continuous_zero` `Continuous.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `Continuous.const_smul` `SMulCommClass.continuousConstSMul` `IsTopologicalSemiring.toContinuousMul` `mem_span_of_iInf_ker_le_ker` `nhds_iInf` `nhds_induced` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `Inseparable.eq` `Inseparable.map`
`toSeminormFamily_apply` 📖	mathematical	—	`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` `Real` `Seminorm.instFunLike` `toSeminormFamily` `Norm.norm` `NormedField.toNorm` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `instFunLike` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`Algebra.to_smulCommClass`
`toSeminorm_apply` 📖	mathematical	—	`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` `Real` `Seminorm.instFunLike` `toSeminorm` `Norm.norm` `NormedField.toNorm` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `instFunLike`	—	—
`toSeminorm_ball_zero` 📖	mathematical	—	`Seminorm.ball` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `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` `toSeminorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `setOf` `Real` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `instFunLike`	—	`Seminorm.ball_zero_eq`
`toSeminorm_comp` 📖	mathematical	—	`Seminorm.comp` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHomIsometric.ids` `toSeminorm` `comp` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `RingHomCompTriple.ids`	—	`Seminorm.ext` `RingHomIsometric.ids` `RingHomCompTriple.ids`
`weakBilin_withSeminorms` 📖	mathematical	—	`WithSeminorms` `WeakBilin` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `AddCommGroup.toAddCommMonoid` `WeakBilin.instAddCommGroup` `instModuleWeakBilin` `toSeminormFamily` `WeakBilin.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`Algebra.to_smulCommClass` `WithSeminorms.congr_equiv` `RingHomIsometric.ids` `RingHomCompTriple.ids` `withSeminorms_induced` `withSeminorms_pi` `norm_withSeminorms`

WeakBilin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyConvexSpace` 📖	mathematical	—	`LocallyConvexSpace` `Real` `WeakBilin` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `AddCommGroup.toAddCommMonoid` `Real.semiring` `Real.partialOrder` `instAddCommMonoidWeakBilin` `instModule'` `Real.instCommSemiring` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`Algebra.to_smulCommClass` `WithSeminorms.toLocallyConvexSpace` `instIsScalarTower` `LinearMap.weakBilin_withSeminorms`

---

← Back to Index