Completeness

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

Statistics

Metric	Count
Definitions ofMemClosureImageCoeBounded, ofTendstoOfBoundedRange	2
Theorems isClosed_image_coe_closedBall, isClosed_image_coe_of_bounded_of_weak_closed, isCompact_closure_image_coe_of_bounded, isCompact_image_coe_closedBall, isCompact_image_coe_of_bounded_of_closed_image, isCompact_image_coe_of_bounded_of_weak_closed, is_weak_closed_closedBall, ofMemClosureImageCoeBounded_apply, ofTendstoOfBoundedRange_apply, tendsto_of_tendsto_pointwise_of_cauchySeq	10
Total	12

ContinuousLinearMap

Definitions

Name	Category	Theorems
ofMemClosureImageCoeBounded 📖	CompOp	1 math math: ofMemClosureImageCoeBounded_apply
ofTendstoOfBoundedRange 📖	CompOp	1 math math: ofTendstoOfBoundedRange_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_image_coe_closedBall 📖	mathematical	—	IsClosed Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.image ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DFunLike.coe funLike Metric.closedBall toPseudoMetricSpace	—	isClosed_image_coe_of_bounded_of_weak_closed Metric.isBounded_closedBall is_weak_closed_closedBall
isClosed_image_coe_of_bounded_of_weak_closed 📖	mathematical	Bornology.IsBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule PseudoMetricSpace.toBornology toPseudoMetricSpace Set Set.instMembership	IsClosed Pi.topologicalSpace Set.image DFunLike.coe funLike	—	isClosed_of_closure_subset
isCompact_closure_image_coe_of_bounded 📖	mathematical	Bornology.IsBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule PseudoMetricSpace.toBornology toPseudoMetricSpace	IsCompact Pi.topologicalSpace closure Set.image DFunLike.coe funLike	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Bornology.IsBounded.isCompact_closure LipschitzWith.isBounded_image RingHomIsometric.ids lipschitz IsCompact.closure_of_subset instR1SpaceForall instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace isCompact_pi_infinite Set.image_subset_iff subset_closure Set.mem_image_of_mem
isCompact_image_coe_closedBall 📖	mathematical	—	IsCompact Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.image ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DFunLike.coe funLike Metric.closedBall toPseudoMetricSpace	—	isCompact_image_coe_of_bounded_of_weak_closed Metric.isBounded_closedBall is_weak_closed_closedBall
isCompact_image_coe_of_bounded_of_closed_image 📖	mathematical	Bornology.IsBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule PseudoMetricSpace.toBornology toPseudoMetricSpace	IsCompact Pi.topologicalSpace Set.image DFunLike.coe funLike	—	isCompact_closure_image_coe_of_bounded IsClosed.closure_eq
isCompact_image_coe_of_bounded_of_weak_closed 📖	mathematical	Bornology.IsBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule PseudoMetricSpace.toBornology toPseudoMetricSpace Set Set.instMembership	IsCompact Pi.topologicalSpace Set.image DFunLike.coe funLike	—	isCompact_image_coe_of_bounded_of_closed_image isClosed_image_coe_of_bounded_of_weak_closed
is_weak_closed_closedBall 📖	—	Set Set.instMembership closure Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.image ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DFunLike.coe funLike Metric.closedBall toPseudoMetricSpace	—	—	Metric.nonempty_closedBall Set.Nonempty.of_image closure_nonempty_iff mem_closedBall_iff_norm opNorm_le_bound IsClosed.preimage Continuous.norm Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_apply continuous_const isClosed_Iic instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal IsClosed.closure_subset_iff Set.image_subset_iff le_of_opNorm_le
ofMemClosureImageCoeBounded_apply 📖	mathematical	Bornology.IsBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule PseudoMetricSpace.toBornology toPseudoMetricSpace Set Set.instMembership closure Pi.topologicalSpace Set.image DFunLike.coe funLike	ofMemClosureImageCoeBounded	—	—
ofTendstoOfBoundedRange_apply 📖	mathematical	Filter.Tendsto DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike nhds Pi.topologicalSpace Bornology.IsBounded PseudoMetricSpace.toBornology toPseudoMetricSpace Set.range	ofTendstoOfBoundedRange	—	—
tendsto_of_tendsto_pointwise_of_cauchySeq 📖	mathematical	Filter.Tendsto DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike Filter.atTop Nat.instPreorder nhds Pi.topologicalSpace CauchySeq uniformSpace SeminormedAddCommGroup.to_isUniformAddGroup	topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup	—	SeminormedAddCommGroup.to_isUniformAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup cauchySeq_iff_le_tendsto_0 Filter.Tendsto.norm Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub tendsto_const_nhds tendsto_pi_nhds le_of_tendsto instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.eventually_atTop le_of_opNorm_le le_rfl tendsto_iff_norm_sub_tendsto_zero squeeze_zero norm_nonneg opNorm_le_bound

---

← Back to Index