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 NormedAddCommGroup.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 NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instUniformSpace NormedAddCommGroup.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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousLinearMap.topologicalAddGroup RingHomIsometric.ids Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMultilinearMap.instIsTopologicalAddGroup SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring 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