Documentation Verification Report

WeakDual

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

Statistics

Metric	Count
Definitions `WeakDual`, `instAddCommGroup`, `instDistribMulAction`, `instModule'`, `instMulAction`, `instAddCommGroup`, `instModule'`, `map`, `instAddCommMonoidWeakDual`, `instAddCommMonoidWeakSpace`, `instContinuousAddWeakDual`, `instContinuousAddWeakSpace`, `instContinuousLinearMapClassWeakDual`, `instFunLikeWeakDual`, `instInhabitedWeakDual`, `instModuleWeakDual`, `instModuleWeakSpace`, `instTopologicalSpaceWeakDual`, `instTopologicalSpaceWeakSpace`, `toWeakSpace`, `toWeakSpaceCLM`	21
Theorems `coeFn_continuous`, `continuous_of_continuous_eval`, `eval_continuous`, `instContinuousConstSMul`, `instContinuousSMul`, `instIsTopologicalAddGroup`, `instT2Space`, `coe_map`, `instContinuousSMul`, `instIsScalarTower`, `instIsTopologicalAddGroup`, `isOpen_of_isOpen`, `map_apply`, `isOpenMap_toWeakSpace_symm`, `tendsto_iff_forall_eval_tendsto_topDualPairing`, `toWeakSpaceCLM_bijective`, `toWeakSpaceCLM_eq_toWeakSpace`	17
Total	38

WeakDual

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	1 math math: `instIsTopologicalAddGroup`
`instDistribMulAction` 📖	CompOp	2 math math: `instContinuousConstSMul`, `instContinuousSMul`
`instModule'` 📖	CompOp	14 math math: `NormedSpace.Dual.toWeakDual_continuous`, `toStrongDual_inj`, `StrongDual.toWeakDual_inj`, `coe_toStrongDual`, `isCompact_closedBall`, `PointwiseConvergenceCLM.equivWeakDual_apply`, `PointwiseConvergenceCLM.equivWeakDual_symm_apply`, `isSeqCompact_closedBall`, `isClosed_closedBall`, `CharacterSpace.norm_le_norm_one`, `StrongDual.coe_toWeakDual`, `toStrongDual_apply`, `NormedSpace.Dual.coe_toWeakDual`, `NormedSpace.Dual.toWeakDual_inj`
`instMulAction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_continuous` 📖	mathematical	—	`Continuous` `WeakDual` `instTopologicalSpaceWeakDual` `Pi.topologicalSpace` `DFunLike.coe` `instFunLikeWeakDual`	—	`continuous_induced_dom`
`continuous_of_continuous_eval` 📖	mathematical	`Continuous` `DFunLike.coe` `WeakDual` `instFunLikeWeakDual`	`instTopologicalSpaceWeakDual`	—	`continuous_induced_rng` `continuous_pi_iff`
`eval_continuous` 📖	mathematical	—	`Continuous` `WeakDual` `instTopologicalSpaceWeakDual` `DFunLike.coe` `instFunLikeWeakDual`	—	`continuous_pi_iff` `coeFn_continuous`
`instContinuousConstSMul` 📖	mathematical	—	`ContinuousConstSMul` `WeakDual` `instTopologicalSpaceWeakDual` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidWeakDual` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instDistribMulAction`	—	`continuous_induced_rng` `Continuous.const_smul` `Algebra.to_smulCommClass` `instContinuousConstSMulForall` `WeakBilin.coeFn_continuous`
`instContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `WeakDual` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidWeakDual` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instDistribMulAction` `ContinuousSMul.continuousConstSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instTopologicalSpaceWeakDual`	—	`ContinuousSMul.continuousConstSMul` `continuous_induced_rng` `Continuous.smul` `instContinuousSMulForall` `continuous_fst` `Continuous.comp` `Algebra.to_smulCommClass` `WeakBilin.coeFn_continuous` `continuous_snd`
`instIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `WeakDual` `CommRing.toCommSemiring` `IsTopologicalAddGroup.toContinuousAdd` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceWeakDual` `AddCommGroup.toAddGroup` `instAddCommGroup`	—	`WeakBilin.instIsTopologicalAddGroup` `Algebra.to_smulCommClass` `IsTopologicalAddGroup.toContinuousAdd`
`instT2Space` 📖	mathematical	—	`T2Space` `WeakDual` `instTopologicalSpaceWeakDual`	—	`Topology.IsEmbedding.t2Space` `Pi.t2Space` `Algebra.to_smulCommClass` `WeakBilin.isEmbedding` `ContinuousLinearMap.coe_injective`

WeakSpace

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	2 math math: `instIsTopologicalAddGroup`, `toWeakSpace_closedConvexHull_eq`
`instModule'` 📖	CompOp	9 math math: `map_apply`, `toWeakSpaceCLM_bijective`, `isOpenMap_toWeakSpace_symm`, `Convex.toWeakSpace_closure`, `toWeakSpace_closedConvexHull_eq`, `instContinuousSMul`, `coe_map`, `toWeakSpaceCLM_eq_toWeakSpace`, `instIsScalarTower`
`map` 📖	CompOp	2 math math: `map_apply`, `coe_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_map` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `WeakSpace` `instTopologicalSpaceWeakSpace` `instAddCommMonoidWeakSpace` `instModule'` `ContinuousLinearMap.funLike` `map`	—	—
`instContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `WeakSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidWeakSpace` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `instModule'` `instTopologicalSpaceWeakSpace`	—	`WeakBilin.instContinuousSMul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `WeakSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommMonoid.toAddMonoid` `instAddCommMonoidWeakSpace` `instModule'`	—	`WeakBilin.instIsScalarTower` `Algebra.to_smulCommClass`
`instIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `WeakSpace` `CommRing.toCommSemiring` `IsTopologicalAddGroup.toContinuousAdd` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceWeakSpace` `AddCommGroup.toAddGroup` `instAddCommGroup`	—	`WeakBilin.instIsTopologicalAddGroup` `Algebra.to_smulCommClass` `IsTopologicalAddGroup.toContinuousAdd`
`isOpen_of_isOpen` 📖	—	`IsOpen` `WeakSpace` `instTopologicalSpaceWeakSpace` `Set.image` `DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instAddCommMonoidWeakSpace` `instModule'` `ContinuousLinearMap.funLike` `toWeakSpaceCLM`	—	—	`RingHomInvPair.ids` `Set.image_congr` `toWeakSpaceCLM_eq_toWeakSpace` `Set.image_image` `LinearEquiv.symm_apply_apply` `Set.image_id'` `isOpenMap_toWeakSpace_symm`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `WeakSpace` `instTopologicalSpaceWeakSpace` `instAddCommMonoidWeakSpace` `instModule'` `ContinuousLinearMap.funLike` `map`	—	—

(root)

Definitions

Name	Category	Theorems
`WeakDual` 📖	CompOp	76 math math: `Ideal.toCharacterSpace_apply_eq_zero_of_mem`, `WeakDual.isCompact_polar`, `MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply`, `WeakDual.isClosed_image_polar_of_mem_nhds`, `WeakDual.CharacterSpace.instIsEmpty`, `StarAlgebra.elemental.characterSpaceToSpectrum_coe`, `WeakDual.CharacterSpace.apply_mem_spectrum`, `WeakDual.CharacterSpace.ext_iff`, `WeakDual.CharacterSpace.union_zero_isClosed`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `NormedSpace.Dual.toWeakDual_continuous`, `gelfandTransform_bijective`, `MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN`, `WeakDual.toStrongDual_inj`, `MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto`, `StrongDual.toWeakDual_inj`, `WeakDual.instContinuousConstSMul`, `WeakDual.coe_toStrongDual`, `spectrum.gelfandTransform_eq`, `WeakDual.CharacterSpace.instNonUnitalAlgHomClass`, `WeakDual.CharacterSpace.continuousMapEval_bijective`, `gelfandStarTransform_symm_apply`, `WeakDual.CharacterSpace.homeoEval_naturality`, `WeakDual.isCompact_closedBall`, `StarAlgebra.elemental.bijective_characterSpaceToSpectrum`, `gelfandTransform_map_star`, `WeakDual.CharacterSpace.coe_coe`, `PointwiseConvergenceCLM.equivWeakDual_apply`, `PointwiseConvergenceCLM.equivWeakDual_symm_apply`, `WeakDual.CharacterSpace.coe_toNonUnitalAlgHom`, `WeakDual.instIsTopologicalAddGroup`, `WeakDual.isSeqCompact_closedBall`, `WeakDual.exists_countable_separating`, `WeakDual.CharacterSpace.coe_toCLM`, `WeakDual.CharacterSpace.union_zero`, `WeakDual.polar_def`, `WeakDual.CharacterSpace.compContinuousMap_apply`, `instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial`, `WeakDual.isClosed_closedBall`, `WeakDual.instT2Space`, `WeakDual.coeFn_continuous`, `tendsto_iff_forall_eval_tendsto_topDualPairing`, `WeakDual.CharacterSpace.eq_set_map_one_map_mul`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply`, `MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN`, `WeakDual.isClosed_polar`, `WeakDual.ker_isMaximal`, `WeakDual.CharacterSpace.norm_le_norm_one`, `WeakDual.CharacterSpace.mem_spectrum_iff_exists`, `WeakDual.instContinuousSMul`, `WeakDual.gelfandTransform_apply_apply`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous`, `MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous`, `WeakDual.CharacterSpace.continuousMapEval_apply_apply`, `WeakDual.CharacterSpace.equivAlgHom_coe`, `WeakDual.CharacterSpace.instAlgHomClass`, `MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN`, `StrongDual.coe_toWeakDual`, `WeakDual.toStrongDual_apply`, `gelfandTransform_isometry`, `WeakDual.CharacterSpace.compContinuousMap_comp`, `WeakDual.CharacterSpace.equivAlgHom_symm_coe`, `StarAlgebra.elemental.continuous_characterSpaceToSpectrum`, `WeakDual.isSeqCompact_polar`, `WeakDual.CharacterSpace.exists_apply_eq_zero`, `WeakDual.CharacterSpace.compContinuousMap_id`, `WeakDual.CharacterSpace.isClosed`, `MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN`, `NormedSpace.Dual.coe_toWeakDual`, `WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace`, `NormedSpace.Dual.toWeakDual_inj`, `WeakDual.eval_continuous`, `WeakDual.CharacterSpace.instStarHomClass`, `MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto`, `WeakDual.CharacterSpace.instContinuousLinearMapClass`
`instAddCommMonoidWeakDual` 📖	CompOp	18 math math: `WeakDual.CharacterSpace.union_zero_isClosed`, `NormedSpace.Dual.toWeakDual_continuous`, `WeakDual.toStrongDual_inj`, `StrongDual.toWeakDual_inj`, `WeakDual.instContinuousConstSMul`, `WeakDual.coe_toStrongDual`, `WeakDual.isCompact_closedBall`, `PointwiseConvergenceCLM.equivWeakDual_apply`, `PointwiseConvergenceCLM.equivWeakDual_symm_apply`, `WeakDual.isSeqCompact_closedBall`, `WeakDual.CharacterSpace.union_zero`, `WeakDual.isClosed_closedBall`, `WeakDual.CharacterSpace.norm_le_norm_one`, `WeakDual.instContinuousSMul`, `StrongDual.coe_toWeakDual`, `WeakDual.toStrongDual_apply`, `NormedSpace.Dual.coe_toWeakDual`, `NormedSpace.Dual.toWeakDual_inj`
`instAddCommMonoidWeakSpace` 📖	CompOp	9 math math: `WeakSpace.map_apply`, `toWeakSpaceCLM_bijective`, `isOpenMap_toWeakSpace_symm`, `Convex.toWeakSpace_closure`, `toWeakSpace_closedConvexHull_eq`, `WeakSpace.instContinuousSMul`, `WeakSpace.coe_map`, `toWeakSpaceCLM_eq_toWeakSpace`, `WeakSpace.instIsScalarTower`
`instContinuousAddWeakDual` 📖	CompOp	—
`instContinuousAddWeakSpace` 📖	CompOp	—
`instContinuousLinearMapClassWeakDual` 📖	CompOp	—
`instFunLikeWeakDual` 📖	CompOp	12 math math: `MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply`, `WeakDual.isClosed_image_polar_of_mem_nhds`, `WeakDual.CharacterSpace.coe_coe`, `WeakDual.coeFn_continuous`, `WeakDual.CharacterSpace.eq_set_map_one_map_mul`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply`, `MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN`, `WeakDual.toStrongDual_apply`, `WeakDual.isClosed_image_coe_of_bounded_of_closed`, `MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN`, `WeakDual.eval_continuous`, `MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto`
`instInhabitedWeakDual` 📖	CompOp	—
`instModuleWeakDual` 📖	CompOp	—
`instModuleWeakSpace` 📖	CompOp	—
`instTopologicalSpaceWeakDual` 📖	CompOp	43 math math: `WeakDual.isCompact_polar`, `WeakDual.CharacterSpace.union_zero_isClosed`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `WeakDual.continuous_of_continuous_eval`, `NormedSpace.Dual.toWeakDual_continuous`, `gelfandTransform_bijective`, `MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto`, `WeakDual.instContinuousConstSMul`, `spectrum.gelfandTransform_eq`, `WeakDual.CharacterSpace.continuousMapEval_bijective`, `gelfandStarTransform_symm_apply`, `WeakDual.CharacterSpace.homeoEval_naturality`, `WeakDual.isCompact_closedBall`, `gelfandTransform_map_star`, `PointwiseConvergenceCLM.equivWeakDual_apply`, `PointwiseConvergenceCLM.equivWeakDual_symm_apply`, `WeakDual.instIsTopologicalAddGroup`, `WeakDual.isSeqCompact_closedBall`, `WeakDual.exists_countable_separating`, `WeakDual.CharacterSpace.compContinuousMap_apply`, `WeakDual.isClosed_closedBall`, `WeakDual.instT2Space`, `WeakDual.coeFn_continuous`, `tendsto_iff_forall_eval_tendsto_topDualPairing`, `WeakDual.isClosed_polar`, `NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology`, `WeakDual.instContinuousSMul`, `WeakDual.isCompact_of_bounded_of_closed`, `WeakDual.gelfandTransform_apply_apply`, `MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous`, `MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous`, `WeakDual.CharacterSpace.continuousMapEval_apply_apply`, `MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN`, `WeakDual.isSeqCompact_of_isBounded_of_isClosed`, `gelfandTransform_isometry`, `WeakDual.CharacterSpace.compContinuousMap_comp`, `StarAlgebra.elemental.continuous_characterSpaceToSpectrum`, `WeakDual.isSeqCompact_polar`, `WeakDual.CharacterSpace.compContinuousMap_id`, `WeakDual.CharacterSpace.isClosed`, `WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace`, `WeakDual.eval_continuous`
`instTopologicalSpaceWeakSpace` 📖	CompOp	9 math math: `WeakSpace.map_apply`, `toWeakSpaceCLM_bijective`, `WeakSpace.instIsTopologicalAddGroup`, `isOpenMap_toWeakSpace_symm`, `Convex.toWeakSpace_closure`, `toWeakSpace_closedConvexHull_eq`, `WeakSpace.instContinuousSMul`, `WeakSpace.coe_map`, `toWeakSpaceCLM_eq_toWeakSpace`
`toWeakSpace` 📖	CompOp	4 math math: `isOpenMap_toWeakSpace_symm`, `Convex.toWeakSpace_closure`, `toWeakSpace_closedConvexHull_eq`, `toWeakSpaceCLM_eq_toWeakSpace`
`toWeakSpaceCLM` 📖	CompOp	2 math math: `toWeakSpaceCLM_bijective`, `toWeakSpaceCLM_eq_toWeakSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenMap_toWeakSpace_symm` 📖	mathematical	—	`IsOpenMap` `WeakSpace` `instTopologicalSpaceWeakSpace` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instAddCommMonoidWeakSpace` `WeakSpace.instModule'` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `toWeakSpace`	—	`IsOpenMap.of_inverse` `RingHomInvPair.ids` `ContinuousLinearMap.cont` `LinearEquiv.left_inv` `LinearEquiv.right_inv`
`tendsto_iff_forall_eval_tendsto_topDualPairing` 📖	mathematical	—	`Filter.Tendsto` `WeakDual` `nhds` `instTopologicalSpaceWeakDual` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `ContinuousLinearMap` `ContinuousLinearMap.addCommMonoid` `LinearMap.addCommMonoid` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.module` `topDualPairing`	—	`WeakBilin.tendsto_iff_forall_eval_tendsto` `ContinuousLinearMap.coe_injective`
`toWeakSpaceCLM_bijective` 📖	mathematical	—	`Function.Bijective` `WeakSpace` `DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceWeakSpace` `instAddCommMonoidWeakSpace` `WeakSpace.instModule'` `ContinuousLinearMap.funLike` `toWeakSpaceCLM`	—	`LinearEquiv.bijective` `RingHomInvPair.ids`
`toWeakSpaceCLM_eq_toWeakSpace` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `WeakSpace` `instTopologicalSpaceWeakSpace` `instAddCommMonoidWeakSpace` `WeakSpace.instModule'` `ContinuousLinearMap.funLike` `toWeakSpaceCLM` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `toWeakSpace`	—	—

---

← Back to Index