Compact

📁 Source: Mathlib/Analysis/Normed/Operator/Compact.lean

Statistics

Metric	Count
Definitions `mkOfIsCompactOperator`, `IsCompactOperator`, `compactOperator`	3
Theorems `coe_mkOfIsCompactOperator`, `mkOfIsCompactOperator_mem_compactOperator`, `mkOfIsCompactOperator_to_linearMap`, `add`, `clm_comp`, `codRestrict`, `comp_clm`, `continuous`, `continuous_comp`, `image_ball_subset_compact`, `image_closedBall_subset_compact`, `image_subset_compact_of_bounded`, `image_subset_compact_of_isVonNBounded`, `isCompact_closure_image_ball`, `isCompact_closure_image_closedBall`, `isCompact_closure_image_of_bounded`, `isCompact_closure_image_of_isVonNBounded`, `neg`, `restrict`, `restrict'`, `smul`, `smul_iff`, `smul_iff₀`, `smul_isUnit_iff`, `smul_unit_iff`, `sub`, `compactOperator_topologicalClosure`, `isClosed_setOf_isCompactOperator`, `isCompactOperator_iff_exists_mem_nhds_image_subset_compact`, `isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image`, `isCompactOperator_iff_image_ball_subset_compact`, `isCompactOperator_iff_image_closedBall_subset_compact`, `isCompactOperator_iff_isCompact_closure_image_ball`, `isCompactOperator_iff_isCompact_closure_image_closedBall`, `isCompactOperator_of_tendsto`, `isCompactOperator_zero`	36
Total	39

ContinuousLinearMap

Definitions

Name	Category	Theorems
`mkOfIsCompactOperator` 📖	CompOp	3 math math: `mkOfIsCompactOperator_mem_compactOperator`, `coe_mkOfIsCompactOperator`, `mkOfIsCompactOperator_to_linearMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mkOfIsCompactOperator` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`ContinuousLinearMap` `funLike` `mkOfIsCompactOperator`	—	—
`mkOfIsCompactOperator_mem_compactOperator` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`ContinuousLinearMap` `Submodule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submodule.setLike` `compactOperator` `mkOfIsCompactOperator`	—	—
`mkOfIsCompactOperator_to_linearMap` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`toLinearMap` `mkOfIsCompactOperator`	—	—

IsCompactOperator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsCompact.add` `Filter.mem_of_superset` `Filter.inter_mem` `Set.add_mem_add`
`clm_comp` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	—	`continuous_comp` `ContinuousLinearMap.continuous`
`codRestrict` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike`	`Set.Elem` `SetLike.coe` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.codRestrict`	—	`Topology.IsClosedEmbedding.isCompact_preimage` `IsClosed.isClosedEmbedding_subtypeVal`
`comp_clm` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	—	`Continuous.tendsto` `ContinuousLinearMap.continuous` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`continuous` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Continuous`	—	`continuous_of_continuousAt_zero` `IsTopologicalAddGroup.toContinuousAdd` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Absorbs.exists_pos` `TotallyBounded.isVonNBounded` `isUniformAddGroup_of_addCommGroup` `IsCompact.totallyBounded` `map_zero` `AddMonoidHomClass.toZeroHomClass` `NormedField.exists_lt_norm` `ne_zero_of_norm_ne_zero` `LT.lt.ne` `LT.lt.trans` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Set.subset_smul_set_iff₀` `map_ne_zero` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `RingHomIsometric.norm_map` `LT.lt.le` `Filter.mem_of_superset` `IsUnit.inv` `Ne.isUnit` `Filter.mem_map` `IsUnit.preimage_smul_setₛₗ` `MonoidWithZeroHomClass.toMonoidHomClass` `SemilinearMapClass.toMulActionSemiHomClass` `set_smul_mem_nhds_zero_iff` `inv_ne_zero`
`continuous_comp` 📖	—	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Continuous`	—	—	`IsCompact.image` `Filter.mem_of_superset` `Set.preimage_comp` `Set.preimage_mono` `Set.subset_preimage_image`
`image_ball_subset_compact` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike`	`IsCompact` `Set` `Set.instHasSubset` `Set.image` `Metric.ball`	—	`image_subset_compact_of_isVonNBounded` `NormedSpace.isVonNBounded_ball`
`image_closedBall_subset_compact` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike`	`IsCompact` `Set` `Set.instHasSubset` `Set.image` `Metric.closedBall`	—	`image_subset_compact_of_isVonNBounded` `NormedSpace.isVonNBounded_closedBall`
`image_subset_compact_of_bounded` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`IsCompact` `Set` `Set.instHasSubset` `Set.image`	—	`image_subset_compact_of_isVonNBounded` `NormedSpace.isVonNBounded_iff`
`image_subset_compact_of_isVonNBounded` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `LinearMap.instFunLike` `Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`IsCompact` `Set` `Set.instHasSubset` `Set.image`	—	`Absorbs.exists_pos` `NormedField.exists_lt_norm` `ne_zero_of_norm_ne_zero` `LT.lt.ne` `LT.lt.trans` `IsCompact.image` `Continuous.const_smul` `continuous_id` `Set.image_subset_iff` `IsUnit.preimage_smul_setₛₗ` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Ne.isUnit` `LT.lt.le`
`isCompact_closure_image_ball` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike`	`IsCompact` `closure` `Set.image` `Metric.ball`	—	`isCompact_closure_image_of_isVonNBounded` `NormedSpace.isVonNBounded_ball`
`isCompact_closure_image_closedBall` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike`	`IsCompact` `closure` `Set.image` `Metric.closedBall`	—	`isCompact_closure_image_of_isVonNBounded` `NormedSpace.isVonNBounded_closedBall`
`isCompact_closure_image_of_bounded` 📖	mathematical	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`IsCompact` `closure` `Set.image`	—	`isCompact_closure_image_of_isVonNBounded` `NormedSpace.isVonNBounded_iff`
`isCompact_closure_image_of_isVonNBounded` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `LinearMap.instFunLike` `Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`IsCompact` `closure` `Set.image`	—	`image_subset_compact_of_isVonNBounded` `IsCompact.closure_of_subset` `T2Space.r1Space`
`neg` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsCompact.neg` `Filter.mem_of_superset` `Set.neg_mem_neg`
`restrict` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Submodule` `SetLike.instMembership` `Submodule.setLike`	`Submodule.zero` `instTopologicalSpaceSubtype` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.restrict`	—	`codRestrict` `comp_clm` `SetLike.forall`
`restrict'` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Submodule` `SetLike.instMembership` `Submodule.setLike`	`Submodule.zero` `instTopologicalSpaceSubtype` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.restrict`	—	`restrict` `IsComplete.isClosed` `completeSpace_coe_iff_isComplete`
`smul` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Function.hasSMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`IsCompact.image` `Continuous.const_smul` `continuous_id` `Filter.mem_of_superset` `Set.smul_mem_smul_set`
`smul_iff` 📖	mathematical	—	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Function.hasSMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`smul_isUnit_iff` `Group.isUnit`
`smul_iff₀` 📖	mathematical	—	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Function.hasSMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero`	—	`smul_isUnit_iff` `Ne.isUnit`
`smul_isUnit_iff` 📖	mathematical	`IsUnit`	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Function.hasSMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`smul_unit_iff`
`smul_unit_iff` 📖	mathematical	—	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Units` `Units.instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`inv_smul_smul` `smul` `Units.continuousConstSMul`
`sub` 📖	mathematical	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `add` `IsTopologicalAddGroup.toContinuousAdd` `neg` `IsTopologicalAddGroup.toContinuousNeg`

(root)

Definitions

Name	Category	Theorems
`IsCompactOperator` 📖	MathDef	12 math math: `isCompactOperator_iff_isCompact_closure_image_ball`, `isCompactOperator_iff_image_closedBall_subset_compact`, `isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image`, `IsCompactOperator.smul_unit_iff`, `isCompactOperator_iff_isCompact_closure_image_closedBall`, `IsCompactOperator.smul_iff₀`, `isCompactOperator_iff_image_ball_subset_compact`, `IsCompactOperator.smul_isUnit_iff`, `isCompactOperator_zero`, `IsCompactOperator.smul_iff`, `isClosed_setOf_isCompactOperator`, `isCompactOperator_iff_exists_mem_nhds_image_subset_compact`
`compactOperator` 📖	CompOp	2 math math: `ContinuousLinearMap.mkOfIsCompactOperator_mem_compactOperator`, `compactOperator_topologicalClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactOperator_topologicalClosure` 📖	mathematical	—	`Submodule.topologicalClosure` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `IsUniformAddGroup.to_topologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `ContinuousLinearMap.continuousConstSMul` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.topologicalAddGroup` `compactOperator`	—	`SetLike.ext'` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `smulCommClass_self` `ContinuousLinearMap.continuousConstSMul` `ContinuousLinearMap.topologicalAddGroup` `IsClosed.closure_eq` `isClosed_setOf_isCompactOperator`
`isClosed_setOf_isCompactOperator` 📖	mathematical	—	`IsClosed` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `IsUniformAddGroup.to_topologicalAddGroup` `AddCommGroup.toAddGroup` `setOf` `IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `ContinuousLinearMap.funLike`	—	`isClosed_of_closure_subset` `IsUniformAddGroup.to_topologicalAddGroup` `totallyBounded_iff_subset_finite_iUnion_nhds_zero` `exists_nhds_zero_half` `IsTopologicalAddGroup.toContinuousAdd` `mem_closure_iff_nhds_zero` `ContinuousLinearMap.topologicalAddGroup` `Filter.HasBasis.mem_of_mem` `ContinuousLinearMap.hasBasis_nhds_zero` `NormedSpace.isVonNBounded_closedBall` `neg_mem_nhds_zero` `IsCompact.totallyBounded` `IsCompactOperator.isCompact_closure_image_closedBall` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `Set.image_subset_iff` `Set.preimage_iUnion₂` `Set.mem_iUnion₂` `Set.mem_preimage` `Set.mem_vadd_set_iff_neg_vadd_mem` `vadd_eq_add` `neg_add_eq_sub` `ContinuousLinearMap.sub_apply` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg` `isCompactOperator_iff_isCompact_closure_image_closedBall` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `TotallyBounded.isCompact_of_isClosed` `TotallyBounded.closure` `isClosed_closure`
`isCompactOperator_iff_exists_mem_nhds_image_subset_compact` 📖	mathematical	—	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set` `Filter` `Filter.instMembership` `nhds` `IsCompact` `Set.instHasSubset` `Set.image`	—	`Set.image_preimage_subset` `Filter.mem_of_superset` `Set.image_subset_iff`
`isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image` 📖	mathematical	—	`IsCompactOperator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set` `Filter` `Filter.instMembership` `nhds` `IsCompact` `closure` `Set.image`	—	`isCompactOperator_iff_exists_mem_nhds_image_subset_compact` `IsCompact.closure_of_subset` `T2Space.r1Space` `subset_closure`
`isCompactOperator_iff_image_ball_subset_compact` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike` `IsCompact` `Set` `Set.instHasSubset` `Set.image` `Metric.ball`	—	`IsCompactOperator.image_ball_subset_compact` `isCompactOperator_iff_exists_mem_nhds_image_subset_compact` `Metric.ball_mem_nhds`
`isCompactOperator_iff_image_closedBall_subset_compact` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike` `IsCompact` `Set` `Set.instHasSubset` `Set.image` `Metric.closedBall`	—	`IsCompactOperator.image_closedBall_subset_compact` `isCompactOperator_iff_exists_mem_nhds_image_subset_compact` `Metric.closedBall_mem_nhds`
`isCompactOperator_iff_isCompact_closure_image_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike` `IsCompact` `closure` `Set.image` `Metric.ball`	—	`IsCompactOperator.isCompact_closure_image_ball` `isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image` `Metric.ball_mem_nhds`
`isCompactOperator_iff_isCompact_closure_image_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike` `IsCompact` `closure` `Set.image` `Metric.closedBall`	—	`IsCompactOperator.isCompact_closure_image_closedBall` `isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image` `Metric.closedBall_mem_nhds`
`isCompactOperator_of_tendsto` 📖	—	`Filter.Tendsto` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `nhds` `ContinuousLinearMap.topologicalSpace` `IsUniformAddGroup.to_topologicalAddGroup` `AddCommGroup.toAddGroup` `Filter.Eventually` `IsCompactOperator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `ContinuousLinearMap.funLike`	—	—	`IsUniformAddGroup.to_topologicalAddGroup` `IsClosed.mem_of_tendsto` `isClosed_setOf_isCompactOperator`
`isCompactOperator_zero` 📖	mathematical	—	`IsCompactOperator` `Pi.instZero`	—	`isCompact_singleton` `Filter.mem_of_superset` `Filter.univ_mem`

---

← Back to Index