Documentation Verification Report

Complemented

📁 Source: Mathlib/Analysis/Normed/Module/Complemented.lean

Statistics

Metric	Count
Definitions `equivProdOfSurjectiveOfIsCompl`, `linearProjOfClosedCompl`, `prodEquivOfClosedCompl`	3
Theorems `coe_equivProdOfSurjectiveOfIsCompl`, `equivProdOfSurjectiveOfIsCompl_apply`, `equivProdOfSurjectiveOfIsCompl_toLinearEquiv`, `ker_closedComplemented_of_finiteDimensional_range`, `of_isCompl_isClosed`, `of_quotient_finiteDimensional`, `closedComplemented_of_isClosed`, `closedComplemented_iff_isClosed_exists_isClosed_isCompl`, `coe_continuous_linearProjOfClosedCompl`, `coe_continuous_linearProjOfClosedCompl'`, `coe_prodEquivOfClosedCompl`, `coe_prodEquivOfClosedCompl_symm`	12
Total	15

ContinuousLinearMap

Definitions

Name	Category	Theorems
`equivProdOfSurjectiveOfIsCompl` 📖	CompOp	4 math math: `equivProdOfSurjectiveOfIsCompl_toLinearEquiv`, `coe_equivProdOfSurjectiveOfIsCompl`, `equivProdOfSurjectiveOfIsCompl_apply`, `ImplicitFunctionData.hasStrictFDerivAt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_equivProdOfSurjectiveOfIsCompl` 📖	mathematical	`LinearMap.range` `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` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `toLinearMap` `Top.top` `Submodule` `Submodule.instTop` `IsCompl` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `LinearMap.ker`	`instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `equivProdOfSurjectiveOfIsCompl` `prod`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`
`equivProdOfSurjectiveOfIsCompl_apply` 📖	mathematical	`LinearMap.range` `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` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `toLinearMap` `Top.top` `Submodule` `Submodule.instTop` `IsCompl` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `LinearMap.ker`	`DFunLike.coe` `ContinuousLinearEquiv` `RingHomInvPair.ids` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equivProdOfSurjectiveOfIsCompl` `ContinuousLinearMap` `funLike`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`
`equivProdOfSurjectiveOfIsCompl_toLinearEquiv` 📖	mathematical	`LinearMap.range` `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` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `toLinearMap` `Top.top` `Submodule` `Submodule.instTop` `IsCompl` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `LinearMap.ker`	`ContinuousLinearEquiv.toLinearEquiv` `RingHomInvPair.ids` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `equivProdOfSurjectiveOfIsCompl` `LinearMap.equivProdOfSurjectiveOfIsCompl` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toAddCommGroup`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`
`ker_closedComplemented_of_finiteDimensional_range` 📖	mathematical	—	`Submodule.ClosedComplemented` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `LinearMap.ker` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap`	—	`RingHomSurjective.ids` `LinearMap.mem_range_self` `RingHomCompTriple.ids` `exists_right_inverse_of_surjective` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `instT2SpaceSubtype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Submodule.topologicalAddGroup` `SMulMemClass.continuousSMul` `Submodule.smulMemClass` `LinearMap.range_rangeRestrict` `ker_codRestrict` `closedComplemented_ker_of_rightInverse` `ext_iff`

Submodule

Definitions

Name	Category	Theorems
`linearProjOfClosedCompl` 📖	CompOp	2 math math: `coe_continuous_linearProjOfClosedCompl'`, `coe_continuous_linearProjOfClosedCompl`
`prodEquivOfClosedCompl` 📖	CompOp	2 math math: `coe_prodEquivOfClosedCompl`, `coe_prodEquivOfClosedCompl_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedComplemented_iff_isClosed_exists_isClosed_isCompl` 📖	mathematical	—	`ClosedComplemented` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `IsClosed` `SetLike.coe` `Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedAddCommGroup.toAddCommGroup` `setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsCompl` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	—	`ClosedComplemented.isClosed` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ClosedComplemented.exists_isClosed_isCompl` `Subtype.t1Space` `ClosedComplemented.of_isCompl_isClosed`
`coe_continuous_linearProjOfClosedCompl` 📖	mathematical	`IsCompl` `Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `instPartialOrder` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `CompleteLattice.toBoundedOrder` `completeLattice`	`ContinuousLinearMap.toLinearMap` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `setLike` `instTopologicalSpaceSubtype` `addCommMonoid` `module` `linearProjOfClosedCompl` `linearProjOfIsCompl` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`coe_continuous_linearProjOfClosedCompl'` 📖	mathematical	`IsCompl` `Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `instPartialOrder` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `ContinuousLinearMap` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `setLike` `instTopologicalSpaceSubtype` `addCommMonoid` `module` `ContinuousLinearMap.funLike` `linearProjOfClosedCompl` `LinearMap` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule` `SeminormedAddCommGroup.toAddCommGroup` `LinearMap.instFunLike` `linearProjOfIsCompl`	—	—
`coe_prodEquivOfClosedCompl` 📖	mathematical	`IsCompl` `Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `instPartialOrder` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `ContinuousLinearEquiv` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `SetLike.instMembership` `setLike` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Prod.instAddCommMonoid` `addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `prodEquivOfClosedCompl` `LinearEquiv` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule` `SeminormedAddCommGroup.toAddCommGroup` `DFinsupp.instEquivLikeLinearEquiv` `prodEquivOfIsCompl`	—	`RingHomInvPair.ids`
`coe_prodEquivOfClosedCompl_symm` 📖	mathematical	`IsCompl` `Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `instPartialOrder` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `ContinuousLinearEquiv` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `setLike` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `prodEquivOfClosedCompl` `LinearEquiv` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule` `SeminormedAddCommGroup.toAddCommGroup` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `prodEquivOfIsCompl`	—	`RingHomInvPair.ids`

Submodule.ClosedComplemented

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isCompl_isClosed` 📖	mathematical	`IsCompl` `Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule.instPartialOrder` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`Submodule.ClosedComplemented` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toAddCommGroup`	—	`Submodule.linearProjOfIsCompl_apply_left`
`of_quotient_finiteDimensional` 📖	mathematical	—	`Submodule.ClosedComplemented` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`Submodule.exists_isCompl` `of_isCompl_isClosed` `Submodule.closed_of_finiteDimensional` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `LinearEquiv.finiteDimensional`

Submodule.IsCompl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedComplemented_of_isClosed` 📖	mathematical	`IsCompl` `Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule.instPartialOrder` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`Submodule.ClosedComplemented` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toAddCommGroup`	—	`Submodule.ClosedComplemented.of_isCompl_isClosed`

---

← Back to Index