Documentation Verification Report

WeakBilin

📁 Source: Mathlib/Topology/Algebra/Module/WeakBilin.lean

Statistics

Metric	Count
Definitions `WeakBilin`, `eval`, `instAddCommGroup`, `instModule'`, `instTopologicalSpace`, `instAddCommMonoidWeakBilin`, `instModuleWeakBilin`	7
Theorems `coeFn_continuous`, `continuous_of_continuous_eval`, `eval_continuous`, `instContinuousAdd`, `instContinuousSMul`, `instIsScalarTower`, `instIsTopologicalAddGroup`, `isEmbedding`, `tendsto_iff_forall_eval_tendsto`	9
Total	16

WeakBilin

Definitions

Name	Category	Theorems
`eval` 📖	CompOp	2 math math: `LinearMap.dualEmbedding_surjective`, `LinearMap.dualEmbedding_injective_of_separatingRight`
`instAddCommGroup` 📖	CompOp	3 math math: `LinearMap.hasBasis_weakBilin`, `LinearMap.weakBilin_withSeminorms`, `instIsTopologicalAddGroup`
`instModule'` 📖	CompOp	2 math math: `locallyConvexSpace`, `instIsScalarTower`
`instTopologicalSpace` 📖	CompOp	15 math math: `isEmbedding`, `LinearMap.dualEmbedding_surjective`, `instContinuousAdd`, `instContinuousSMul`, `LinearMap.hasBasis_weakBilin`, `locallyConvexSpace`, `LinearMap.weakBilin_withSeminorms`, `LinearMap.polar_weak_closed`, `coeFn_continuous`, `tendsto_iff_forall_eval_tendsto`, `eval_continuous`, `continuous_of_continuous_eval`, `LinearMap.polar_isClosed`, `LinearMap.dualEmbedding_injective_of_separatingRight`, `instIsTopologicalAddGroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_continuous` 📖	mathematical	—	`Continuous` `WeakBilin` `instTopologicalSpace` `Pi.topologicalSpace` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`Algebra.to_smulCommClass` `continuous_induced_dom`
`continuous_of_continuous_eval` 📖	mathematical	`Continuous` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	`Continuous` `WeakBilin` `instTopologicalSpace`	—	`Algebra.to_smulCommClass` `continuous_induced_rng` `continuous_pi_iff`
`eval_continuous` 📖	mathematical	—	`Continuous` `WeakBilin` `instTopologicalSpace` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`Algebra.to_smulCommClass` `continuous_pi_iff` `coeFn_continuous`
`instContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `WeakBilin` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidWeakBilin`	—	`Algebra.to_smulCommClass` `continuous_induced_rng` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `Continuous.add` `Pi.continuousAdd'` `Continuous.comp` `coeFn_continuous` `continuous_fst` `continuous_snd`
`instContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `WeakBilin` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidWeakBilin` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `instModuleWeakBilin` `instTopologicalSpace`	—	`Algebra.to_smulCommClass` `continuous_induced_rng` `MulActionSemiHomClass.map_smulₛₗ` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Continuous.smul` `instContinuousSMulForall` `continuous_fst` `Continuous.comp` `coeFn_continuous` `continuous_snd`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `WeakBilin` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidWeakBilin` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `instModuleWeakBilin` `instModule'`	—	`Algebra.to_smulCommClass`
`instIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `WeakBilin` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpace` `AddCommGroup.toAddGroup` `instAddCommGroup`	—	`Algebra.to_smulCommClass` `instContinuousAdd` `continuous_induced_rng` `continuous_pi_iff` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `eval_continuous`
`isEmbedding` 📖	mathematical	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instFunLike`	`Topology.IsEmbedding` `WeakBilin` `instTopologicalSpace` `Pi.topologicalSpace` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`Algebra.to_smulCommClass` `Function.Injective.isEmbedding_induced` `LinearMap.coe_injective`
`tendsto_iff_forall_eval_tendsto` 📖	mathematical	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instFunLike`	`Filter.Tendsto` `WeakBilin` `nhds` `instTopologicalSpace` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`Algebra.to_smulCommClass` `tendsto_pi_nhds` `Topology.IsEmbedding.tendsto_nhds_iff` `isEmbedding`

(root)

Definitions

Name	Category	Theorems
`WeakBilin` 📖	CompOp	16 math math: `WeakBilin.isEmbedding`, `LinearMap.dualEmbedding_surjective`, `WeakBilin.instContinuousAdd`, `WeakBilin.instContinuousSMul`, `LinearMap.hasBasis_weakBilin`, `WeakBilin.locallyConvexSpace`, `WeakBilin.instIsScalarTower`, `LinearMap.weakBilin_withSeminorms`, `LinearMap.polar_weak_closed`, `WeakBilin.coeFn_continuous`, `WeakBilin.tendsto_iff_forall_eval_tendsto`, `WeakBilin.eval_continuous`, `WeakBilin.continuous_of_continuous_eval`, `LinearMap.polar_isClosed`, `LinearMap.dualEmbedding_injective_of_separatingRight`, `WeakBilin.instIsTopologicalAddGroup`
`instAddCommMonoidWeakBilin` 📖	CompOp	6 math math: `LinearMap.dualEmbedding_surjective`, `WeakBilin.instContinuousAdd`, `WeakBilin.instContinuousSMul`, `WeakBilin.locallyConvexSpace`, `WeakBilin.instIsScalarTower`, `LinearMap.dualEmbedding_injective_of_separatingRight`
`instModuleWeakBilin` 📖	CompOp	5 math math: `LinearMap.dualEmbedding_surjective`, `WeakBilin.instContinuousSMul`, `WeakBilin.instIsScalarTower`, `LinearMap.weakBilin_withSeminorms`, `LinearMap.dualEmbedding_injective_of_separatingRight`

---

← Back to Index