CompactConvergenceCLM

📁 Source: Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean

Statistics

Metric	Count
Definitions CompactConvergenceCLM, «term_→L_c[_]_», «term_→SL_c[_]_», postcompCompactConvergenceCLM, precompCompactConvergenceCLM, postcomp_compactConvergenceCLM, precomp_compactConvergenceCLM	7
Theorems continuousSMul, hasBasis_nhds_zero, hasBasis_nhds_zero_of_basis, instContinuousEvalConst, instT2Space, postcompCompactConvergenceCLM_apply, precompCompactConvergenceCLM_apply, postcomp_compactConvergenceCLM_apply, precomp_compactConvergenceCLM_apply	9
Total	16

CompactConvergenceCLM

Definitions

Name	Category	Theorems
«term_→L_c[_]_» 📖	CompOp	—
«term_→SL_c[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul CompactConvergenceCLM UniformSpace.toTopologicalSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformConvergenceCLM.instAddCommGroup setOf Set IsCompact DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformConvergenceCLM.instDistribMulAction Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing UniformConvergenceCLM.instTopologicalSpace	—	UniformConvergenceCLM.continuousSMul TotallyBounded.isVonNBounded IsCompact.totallyBounded
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis CompactConvergenceCLM Set nhds UniformConvergenceCLM.instTopologicalSpace setOf IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid UniformConvergenceCLM.instAddCommGroup Filter Filter.instMembership	—	hasBasis_nhds_zero_of_basis Filter.basis_sets
hasBasis_nhds_zero_of_basis 📖	mathematical	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.HasBasis CompactConvergenceCLM Set nhds UniformConvergenceCLM.instTopologicalSpace setOf IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid UniformConvergenceCLM.instAddCommGroup	—	UniformConvergenceCLM.hasBasis_nhds_zero_of_basis isCompact_empty directedOn_of_sup_mem IsCompact.union
instContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst CompactConvergenceCLM UniformConvergenceCLM.instFunLike setOf Set IsCompact UniformConvergenceCLM.instTopologicalSpace	—	UniformConvergenceCLM.continuousEvalConst Set.sUnion_isCompact_eq_univ
instT2Space 📖	mathematical	—	T2Space CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact	—	UniformConvergenceCLM.t2Space Set.sUnion_isCompact_eq_univ

ContinuousLinearMap

Definitions

Name	Category	Theorems
postcompCompactConvergenceCLM 📖	CompOp	2 math math: postcompCompactConvergenceCLM_apply, postcomp_compactConvergenceCLM_apply
precompCompactConvergenceCLM 📖	CompOp	2 math math: precomp_compactConvergenceCLM_apply, precompCompactConvergenceCLM_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
postcompCompactConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike postcompCompactConvergenceCLM comp	—	smulCommClass_self
precompCompactConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike precompCompactConvergenceCLM comp	—	smulCommClass_self

(root)

Definitions

Name	Category	Theorems
CompactConvergenceCLM 📖	CompOp	11 math math: ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, CompactConvergenceCLM.hasBasis_nhds_zero_of_basis, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, ContinuousLinearMap.postcompCompactConvergenceCLM_apply, CompactConvergenceCLM.hasBasis_nhds_zero, precomp_compactConvergenceCLM_apply, CompactConvergenceCLM.instContinuousEvalConst, CompactConvergenceCLM.instT2Space, ContinuousLinearMap.precompCompactConvergenceCLM_apply, CompactConvergenceCLM.continuousSMul, postcomp_compactConvergenceCLM_apply
postcomp_compactConvergenceCLM 📖	CompOp	—
precomp_compactConvergenceCLM 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
postcomp_compactConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike ContinuousLinearMap.postcompCompactConvergenceCLM ContinuousLinearMap.comp	—	ContinuousLinearMap.postcompCompactConvergenceCLM_apply
precomp_compactConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike ContinuousLinearMap.precompCompactConvergenceCLM ContinuousLinearMap.comp	—	ContinuousLinearMap.precompCompactConvergenceCLM_apply

---

← Back to Index