Documentation Verification Report

ContinuousInverse

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

Statistics

Metric	Count
Definitions `HasLeftInverse`, `complement`, `leftInverse`, `HasRightInverse`, `rightInverse`	5
Theorems `hasLeftInverse`, `hasRightInverse`, `leftInverse_hasLeftInverse`, `rightInverse_hasRightInverse`, `closedComplemented_range`, `comp`, `comp_continuousLinearEquivalence`, `continuousLinearEquivalence_comp`, `injective`, `inl`, `inr`, `isClosed_complement`, `isClosed_range`, `isCompl_complement`, `leftInverse_leftInverse`, `of_comp`, `of_injective_of_finiteDimensional`, `of_injective_of_isClosed_range_of_closedComplement_range`, `of_isInvertible`, `prodMap`, `comp`, `comp_continuousLinearEquivalence`, `continuousLinearEquivalence_comp`, `fst`, `of_comp`, `of_isInvertible`, `of_surjective_of_finiteDimensional`, `prodMap`, `rightInverse_rightInverse`, `snd`, `surjective`	31
Total	36

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLeftInverse` 📖	mathematical	—	`ContinuousLinearMap.HasLeftInverse` `toContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `ContinuousLinearMap.rightInverse_of_comp` `RingHomCompTriple.ids` `coe_symm_comp_coe`
`hasRightInverse` 📖	mathematical	—	`ContinuousLinearMap.HasRightInverse` `toContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `ContinuousLinearMap.rightInverse_of_comp` `RingHomCompTriple.ids` `coe_comp_coe_symm`
`leftInverse_hasLeftInverse` 📖	mathematical	—	`ContinuousLinearMap.HasLeftInverse.leftInverse` `toContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `hasLeftInverse` `symm`	—	`RingHomInvPair.ids` `ContinuousLinearMap.ext` `hasLeftInverse` `apply_symm_apply` `ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse`
`rightInverse_hasRightInverse` 📖	mathematical	—	`ContinuousLinearMap.HasRightInverse.rightInverse` `toContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `hasRightInverse` `symm`	—	`RingHomInvPair.ids` `ContinuousLinearMap.ext` `hasRightInverse` `injective` `apply_symm_apply` `ContinuousLinearMap.HasRightInverse.rightInverse_rightInverse`

ContinuousLinearMap

Definitions

Name	Category	Theorems
`HasLeftInverse` 📖	MathDef	12 math math: `HasLeftInverse.of_isInvertible`, `HasLeftInverse.of_comp`, `HasLeftInverse.comp_continuousLinearEquivalence`, `ContinuousLinearEquiv.hasLeftInverse`, `HasLeftInverse.inl`, `HasLeftInverse.of_injective_of_finiteDimensional`, `HasLeftInverse.prodMap`, `HasLeftInverse.congr`, `HasLeftInverse.comp`, `HasLeftInverse.inr`, `HasLeftInverse.continuousLinearEquivalence_comp`, `HasLeftInverse.of_injective_of_isClosed_range_of_closedComplement_range`
`HasRightInverse` 📖	MathDef	11 math math: `HasRightInverse.comp_continuousLinearEquivalence`, `HasRightInverse.continuousLinearEquivalence_comp`, `ContinuousLinearEquiv.hasRightInverse`, `HasRightInverse.comp`, `HasRightInverse.of_isInvertible`, `HasRightInverse.prodMap`, `HasRightInverse.snd`, `HasRightInverse.of_surjective_of_finiteDimensional`, `HasRightInverse.congr`, `HasRightInverse.fst`, `HasRightInverse.of_comp`

ContinuousLinearMap.HasLeftInverse

Definitions

Name	Category	Theorems
`complement` 📖	CompOp	2 math math: `isClosed_complement`, `isCompl_complement`
`leftInverse` 📖	CompOp	2 math math: `leftInverse_leftInverse`, `ContinuousLinearEquiv.leftInverse_hasLeftInverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedComplemented_range` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`Submodule.ClosedComplemented` `LinearMap.range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `leftInverse_leftInverse`
`comp` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse`	`ContinuousLinearMap.HasLeftInverse` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids`
`comp_continuousLinearEquivalence` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse`	`ContinuousLinearMap.HasLeftInverse` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `comp` `ContinuousLinearEquiv.hasLeftInverse`
`continuousLinearEquivalence_comp` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse`	`ContinuousLinearMap.HasLeftInverse` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `comp` `ContinuousLinearEquiv.hasLeftInverse`
`injective` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse`	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	`leftInverse_leftInverse`
`inl` 📖	mathematical	—	`ContinuousLinearMap.HasLeftInverse` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `ContinuousLinearMap.inl`	—	—
`inr` 📖	mathematical	—	`ContinuousLinearMap.HasLeftInverse` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `ContinuousLinearMap.inr`	—	—
`isClosed_complement` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`IsClosed` `SetLike.coe` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `complement`	—	`Submodule.ClosedComplemented.isClosed_complement` `RingHomSurjective.ids` `Subtype.t1Space` `closedComplemented_range`
`isClosed_range` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`IsClosed` `Set.range` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike`	—	`ContinuousLinearMap.range_toLinearMap` `RingHomSurjective.ids` `LinearMap.coe_range` `RingHomCompTriple.ids` `LinearMap.range_eq_ker_of_leftInverse` `leftInverse_leftInverse` `ContinuousLinearMap.isClosed_ker`
`isCompl_complement` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `complement`	—	`Submodule.ClosedComplemented.isCompl_complement` `RingHomSurjective.ids` `Subtype.t1Space` `closedComplemented_range`
`leftInverse_leftInverse` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse`	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `leftInverse`	—	—
`of_comp` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	`ContinuousLinearMap.HasLeftInverse`	—	`RingHomCompTriple.ids`
`of_injective_of_finiteDimensional` 📖	mathematical	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike`	`ContinuousLinearMap.HasLeftInverse` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	—	`RingHomCompTriple.ids` `LinearMap.exists_leftInverse_of_injective` `LinearMap.ker_eq_bot_of_injective` `LinearMap.continuous_of_finiteDimensional`
`of_injective_of_isClosed_range_of_closedComplement_range` 📖	mathematical	`DFunLike.coe` `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.funLike` `Submodule.ClosedComplemented` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `LinearMap.range` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap`	`ContinuousLinearMap.HasLeftInverse` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule`	—	`RingHomSurjective.ids` `ContinuousLinearMap.ker_codRestrict` `LinearMap.ker_eq_bot` `RingHomCompTriple.ids`
`of_isInvertible` 📖	mathematical	`ContinuousLinearMap.IsInvertible`	`ContinuousLinearMap.HasLeftInverse`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.hasLeftInverse`
`prodMap` 📖	mathematical	`ContinuousLinearMap.HasLeftInverse`	`ContinuousLinearMap.HasLeftInverse` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `ContinuousLinearMap.prodMap`	—	`Zero.instNonempty`

ContinuousLinearMap.HasRightInverse

Definitions

Name	Category	Theorems
`rightInverse` 📖	CompOp	2 math math: `rightInverse_rightInverse`, `ContinuousLinearEquiv.rightInverse_hasRightInverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`ContinuousLinearMap.HasRightInverse`	`ContinuousLinearMap.HasRightInverse` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids`
`comp_continuousLinearEquivalence` 📖	mathematical	`ContinuousLinearMap.HasRightInverse`	`ContinuousLinearMap.HasRightInverse` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `comp` `ContinuousLinearEquiv.hasRightInverse`
`continuousLinearEquivalence_comp` 📖	mathematical	`ContinuousLinearMap.HasRightInverse`	`ContinuousLinearMap.HasRightInverse` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `comp` `ContinuousLinearEquiv.hasRightInverse`
`fst` 📖	mathematical	—	`ContinuousLinearMap.HasRightInverse` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `ContinuousLinearMap.fst`	—	—
`of_comp` 📖	mathematical	`ContinuousLinearMap.HasRightInverse` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	`ContinuousLinearMap.HasRightInverse`	—	`RingHomCompTriple.ids`
`of_isInvertible` 📖	mathematical	`ContinuousLinearMap.IsInvertible`	`ContinuousLinearMap.HasRightInverse`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.hasRightInverse`
`of_surjective_of_finiteDimensional` 📖	mathematical	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike`	`ContinuousLinearMap.HasRightInverse` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	—	`RingHomCompTriple.ids` `LinearMap.exists_rightInverse_of_surjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `LinearMap.range_eq_top_of_surjective` `RingHomSurjective.ids` `LinearMap.continuous_of_finiteDimensional`
`prodMap` 📖	mathematical	`ContinuousLinearMap.HasRightInverse`	`ContinuousLinearMap.HasRightInverse` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `ContinuousLinearMap.prodMap`	—	`Zero.instNonempty`
`rightInverse_rightInverse` 📖	mathematical	`ContinuousLinearMap.HasRightInverse`	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `rightInverse`	—	—
`snd` 📖	mathematical	—	`ContinuousLinearMap.HasRightInverse` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `ContinuousLinearMap.snd`	—	—
`surjective` 📖	mathematical	`ContinuousLinearMap.HasRightInverse`	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	`rightInverse_rightInverse`

---

← Back to Index