CompleteCodomain

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

Statistics

Metric	Count
Definitions	0
Theorems completeSpace_continuousLinearMap_iff, completeSpace_continuousMultilinearMap_iff, completeSpace_of_completeSpace_continuousLinearMap, completeSpace_of_completeSpace_continuousMultilinearMap	4
Total	4

SeparatingDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completeSpace_continuousLinearMap_iff 📖	mathematical	—	CompleteSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup	—	SeminormedAddCommGroup.to_isUniformAddGroup completeSpace_of_completeSpace_continuousLinearMap ContinuousLinearMap.instCompleteSpace SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace
completeSpace_continuousMultilinearMap_iff 📖	mathematical	SeparatingDual NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedSpace.toModule	CompleteSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instUniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup	—	SeminormedAddCommGroup.to_isUniformAddGroup completeSpace_of_completeSpace_continuousMultilinearMap ContinuousMultilinearMap.instCompleteSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedAddCommGroup.toIsTopologicalAddGroup FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.instFirstCountableTopologyForallOfCountable Finite.to_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace
completeSpace_of_completeSpace_continuousLinearMap 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	SeminormedAddCommGroup.to_isUniformAddGroup Metric.complete_of_cauchySeq_tendsto exists_ne exists_eq_one IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring ContinuousLinearMap.topologicalAddGroup RingHomIsometric.ids Algebra.to_smulCommClass Ring.uniformContinuousConstSMul IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul LipschitzWith.cauchySeq_comp ContinuousLinearMap.lipschitz cauchy_iff_exists_le_nhds Filter.map_neBot Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Continuous.eval_const ContinuousLinearMap.instContinuousEvalConst IsBoundedSMul.continuousSMul continuous_id' Filter.Tendsto.comp Continuous.tendsto one_smul
completeSpace_of_completeSpace_continuousMultilinearMap 📖	mathematical	SeparatingDual NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedSpace.toModule	CompleteSpace	—	SeminormedAddCommGroup.to_isUniformAddGroup Metric.complete_of_cauchySeq_tendsto exists_eq_one IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing nonempty_fintype SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring ContinuousMultilinearMap.instIsTopologicalAddGroup Ring.uniformContinuousConstSMul IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul LipschitzWith.cauchySeq_comp RingHomIsometric.ids ContinuousLinearMap.lipschitz cauchy_iff_exists_le_nhds Filter.map_neBot Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.comp Continuous.tendsto ContinuousEvalConst.continuous_eval_const ContinuousMultilinearMap.instContinuousEvalConstForall IsBoundedSMul.continuousSMul Finset.prod_const_one one_smul

---

← Back to Index