WeakOperatorTopology

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

Statistics

Metric	Count
Definitions toWOT, ContinuousLinearMapWOT, toWOTCLM, inducingFn, instAddCommGroup, instFunLike, instModule, instTopologicalSpace, instUniformSpace, seminorm, seminormFamily, «term_→SWOT[_]_», «term_→WOT[_]_»	13
Theorems toWOT_apply, continuous_toWOT, add_apply, continuous_dual_apply, continuous_inducingFn, continuous_of_dual_apply_continuous, ext, ext_dual, ext_dual_iff, ext_iff, hasBasis_seminorms, inducingFn_apply, instContinuousAdd, instContinuousLinearMapClass, instContinuousNeg, instContinuousSMul, instIsTopologicalAddGroup, instIsUniformAddGroup, instLocallyConvexSpace, instT3Space, isEmbedding_inducingFn, isInducing_inducingFn, le_nhds_iff_forall_dual_apply_le_nhds, neg_apply, smul_apply, sub_apply, tendsto_iff_forall_dual_apply_tendsto, withSeminorms, zero_apply	29
Total	42

ContinuousLinearMap

Definitions

Name	Category	Theorems
toWOT 📖	CompOp	2 math math: ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT, toWOT_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toWOT_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMapWOT.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap AddCommGroup.toAddCommMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMapWOT.instAddCommGroup module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMapWOT.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toWOT funLike	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self

ContinuousLinearMapWOT

Definitions

Name	Category	Theorems
inducingFn 📖	CompOp	4 math math: inducingFn_apply, isInducing_inducingFn, isEmbedding_inducingFn, continuous_inducingFn
instAddCommGroup 📖	CompOp	19 math math: neg_apply, withSeminorms, instIsUniformAddGroup, inducingFn_apply, instLocallyConvexSpace, smul_apply, instIsTopologicalAddGroup, isInducing_inducingFn, hasBasis_seminorms, isEmbedding_inducingFn, instContinuousSMul, instContinuousAdd, continuous_inducingFn, add_apply, sub_apply, instContinuousNeg, ContinuousLinearMap.continuous_toWOT, ContinuousLinearMap.toWOT_apply, zero_apply
instFunLike 📖	CompOp	16 math math: neg_apply, le_nhds_iff_forall_inner_apply_le_nhds, tendsto_iff_forall_inner_apply_tendsto, le_nhds_iff_forall_dual_apply_le_nhds, inducingFn_apply, smul_apply, ext_dual_iff, add_apply, ext_iff, instContinuousLinearMapClass, sub_apply, continuous_dual_apply, tendsto_iff_forall_dual_apply_tendsto, ContinuousLinearMap.toWOT_apply, zero_apply, ext_inner_iff
instModule 📖	CompOp	10 math math: withSeminorms, inducingFn_apply, smul_apply, isInducing_inducingFn, hasBasis_seminorms, isEmbedding_inducingFn, instContinuousSMul, continuous_inducingFn, ContinuousLinearMap.continuous_toWOT, ContinuousLinearMap.toWOT_apply
instTopologicalSpace 📖	CompOp	18 math math: le_nhds_iff_forall_inner_apply_le_nhds, tendsto_iff_forall_inner_apply_tendsto, withSeminorms, le_nhds_iff_forall_dual_apply_le_nhds, instLocallyConvexSpace, instIsTopologicalAddGroup, isInducing_inducingFn, hasBasis_seminorms, isEmbedding_inducingFn, continuous_of_dual_apply_continuous, instContinuousSMul, instContinuousAdd, instT3Space, continuous_inducingFn, continuous_dual_apply, instContinuousNeg, ContinuousLinearMap.continuous_toWOT, tendsto_iff_forall_dual_apply_tendsto
instUniformSpace 📖	CompOp	1 math math: instIsUniformAddGroup
seminorm 📖	CompOp	—
seminormFamily 📖	CompOp	2 math math: withSeminorms, hasBasis_seminorms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup	—	—
continuous_dual_apply 📖	mathematical	—	Continuous ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DFunLike.coe StrongDual AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike	—	continuous_pi_iff continuous_inducingFn
continuous_inducingFn 📖	mathematical	—	Continuous ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpace Pi.topologicalSpace StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommGroup Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instModule Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike inducingFn	—	continuous_induced_dom
continuous_of_dual_apply_continuous 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ContinuousLinearMapWOT instFunLike	instTopologicalSpace	—	continuous_induced_rng continuous_pi_iff
ext 📖	—	DFunLike.coe ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instFunLike	—	—	ContinuousLinearMap.ext
ext_dual 📖	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ContinuousLinearMapWOT instFunLike	—	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul SMulCommClass.symm separatingDual_iff_injective
ext_dual_iff 📖	mathematical	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ContinuousLinearMapWOT instFunLike	—	ext_dual
ext_iff 📖	mathematical	—	DFunLike.coe ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instFunLike	—	ContinuousLinearMap.ext_iff
hasBasis_seminorms 📖	mathematical	—	Filter.HasBasis ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Set nhds instTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup SeminormFamily.basisSets StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid instModule seminormFamily	—	WithSeminorms.hasBasis withSeminorms
inducingFn_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMapWOT AddCommGroup.toAddCommMonoid instAddCommGroup Pi.addCommMonoid StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instModule Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike inducingFn ContinuousLinearMap.funLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike	—	—
instContinuousAdd 📖	mathematical	—	ContinuousAdd ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpace AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup	—	ContinuousAdd.induced SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
instContinuousLinearMapClass 📖	mathematical	—	ContinuousSemilinearMapClass ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instFunLike	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass LinearMap.map_smulₛₗ ContinuousLinearMap.continuous RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
instContinuousNeg 📖	mathematical	—	ContinuousNeg ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpace NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	ContinuousNeg.induced DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Pi.has_continuous_neg' IsTopologicalRing.toContinuousNeg IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
instContinuousSMul 📖	mathematical	—	ContinuousSMul ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instTopologicalSpace	—	ContinuousSMul.induced LinearMap.semilinearMapClass instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpace AddCommGroup.toAddGroup instAddCommGroup	—	instContinuousAdd instContinuousNeg
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instUniformSpace AddCommGroup.toAddGroup instAddCommGroup	—	IsUniformAddGroup.comap Pi.instIsUniformAddGroup SeminormedAddCommGroup.to_isUniformAddGroup DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
instLocallyConvexSpace 📖	mathematical	—	LocallyConvexSpace Real ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid instAddCommGroup instTopologicalSpace	—	WithSeminorms.toLocallyConvexSpace withSeminorms
instT3Space 📖	mathematical	—	T3Space ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpace	—	Topology.IsEmbedding.t3Space instT3SpaceForall T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity isEmbedding_inducingFn
isEmbedding_inducingFn 📖	mathematical	—	Topology.IsEmbedding ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpace Pi.topologicalSpace StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommGroup Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instModule Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike inducingFn	—	Function.Injective.isEmbedding_induced ext_dual_iff
isInducing_inducingFn 📖	mathematical	—	Topology.IsInducing ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpace Pi.topologicalSpace StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommGroup Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instModule Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike inducingFn	—	—
le_nhds_iff_forall_dual_apply_le_nhds 📖	mathematical	—	Filter ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds instTopologicalSpace Filter.map DFunLike.coe StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike	—	tendsto_iff_forall_dual_apply_tendsto
neg_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	—
smul_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule	—	—
sub_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup	—	—
tendsto_iff_forall_dual_apply_tendsto 📖	mathematical	—	Filter.Tendsto ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField nhds instTopologicalSpace DFunLike.coe StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike	—	Topology.IsInducing.tendsto_nhds_iff isInducing_inducingFn
withSeminorms 📖	mathematical	—	WithSeminorms ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid instAddCommGroup instModule seminormFamily instTopologicalSpace	—	Topology.IsInducing.withSeminorms RingHomIsometric.ids WithSeminorms.congr_equiv withSeminorms_pi norm_withSeminorms isInducing_inducingFn
zero_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMapWOT DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	—

ContinuousLinearMapWOT.ContinuousLinearMap

Definitions

Name	Category	Theorems
toWOTCLM 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_toWOT 📖	mathematical	—	Continuous ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousLinearMapWOT ContinuousLinearMap.topologicalSpace ContinuousLinearMapWOT.instTopologicalSpace DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMapWOT.instAddCommGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMapWOT.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ContinuousLinearMap.toWOT	—	ContinuousLinearMapWOT.continuous_of_dual_apply_continuous RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self Continuous.comp ContinuousLinearMap.cont ContinuousEvalConst.continuous_eval_const ContinuousLinearMap.instContinuousEvalConst

(root)

Definitions

Name	Category	Theorems
ContinuousLinearMapWOT 📖	CompOp	29 math math: ContinuousLinearMapWOT.neg_apply, ContinuousLinearMapWOT.le_nhds_iff_forall_inner_apply_le_nhds, ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto, ContinuousLinearMapWOT.withSeminorms, ContinuousLinearMapWOT.instIsUniformAddGroup, ContinuousLinearMapWOT.le_nhds_iff_forall_dual_apply_le_nhds, ContinuousLinearMapWOT.inducingFn_apply, ContinuousLinearMapWOT.instLocallyConvexSpace, ContinuousLinearMapWOT.smul_apply, ContinuousLinearMapWOT.instIsTopologicalAddGroup, ContinuousLinearMapWOT.isInducing_inducingFn, ContinuousLinearMapWOT.hasBasis_seminorms, ContinuousLinearMapWOT.isEmbedding_inducingFn, ContinuousLinearMapWOT.instContinuousSMul, ContinuousLinearMapWOT.instContinuousAdd, ContinuousLinearMapWOT.ext_dual_iff, ContinuousLinearMapWOT.instT3Space, ContinuousLinearMapWOT.continuous_inducingFn, ContinuousLinearMapWOT.add_apply, ContinuousLinearMapWOT.ext_iff, ContinuousLinearMapWOT.instContinuousLinearMapClass, ContinuousLinearMapWOT.sub_apply, ContinuousLinearMapWOT.continuous_dual_apply, ContinuousLinearMapWOT.instContinuousNeg, ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT, ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto, ContinuousLinearMap.toWOT_apply, ContinuousLinearMapWOT.zero_apply, ContinuousLinearMapWOT.ext_inner_iff
«term_→SWOT[_]_» 📖	CompOp	—
«term_→WOT[_]_» 📖	CompOp	—

---

← Back to Index