ContinuousInverse

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

Statistics

Metric	Count
Definitions HasLeftInverse, leftInverse, HasRightInverse, rightInverse	4
Theorems hasLeftInverse, hasRightInverse, leftInverse_hasLeftInverse, rightInverse_hasRightInverse, comp, comp_continuousLinearEquivalence, continuousLinearEquivalence_comp, injective, inl, inr, leftInverse_leftInverse, of_comp, of_injective_of_finiteDimensional, of_isInvertible, prodMap, comp, comp_continuousLinearEquivalence, continuousLinearEquivalence_comp, fst, of_comp, of_isInvertible, of_surjective_of_finiteDimensional, prodMap, rightInverse_rightInverse, snd, surjective	26
Total	30

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	5 math math: HasLeftInverse.of_isInvertible, ContinuousLinearEquiv.hasLeftInverse, HasLeftInverse.inl, HasLeftInverse.of_injective_of_finiteDimensional, HasLeftInverse.inr
HasRightInverse 📖	MathDef	5 math math: ContinuousLinearEquiv.hasRightInverse, HasRightInverse.of_isInvertible, HasRightInverse.snd, HasRightInverse.of_surjective_of_finiteDimensional, HasRightInverse.fst

ContinuousLinearMap.HasLeftInverse

Definitions

Name	Category	Theorems
leftInverse 📖	CompOp	2 math math: leftInverse_leftInverse, ContinuousLinearEquiv.leftInverse_hasLeftInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	ContinuousLinearMap.HasLeftInverse	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomCompTriple.ids
comp_continuousLinearEquivalence 📖	mathematical	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.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	—	—
leftInverse_leftInverse 📖	mathematical	ContinuousLinearMap.HasLeftInverse	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike leftInverse	—	—
of_comp 📖	—	ContinuousLinearMap.HasLeftInverse ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—	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	—	RingHomCompTriple.ids LinearMap.exists_leftInverse_of_injective LinearMap.ker_eq_bot_of_injective LinearMap.continuous_of_finiteDimensional
of_isInvertible 📖	mathematical	ContinuousLinearMap.IsInvertible	ContinuousLinearMap.HasLeftInverse	—	RingHomInvPair.ids ContinuousLinearEquiv.hasLeftInverse
prodMap 📖	mathematical	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.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomCompTriple.ids
comp_continuousLinearEquivalence 📖	mathematical	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.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 📖	—	ContinuousLinearMap.HasRightInverse ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—	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	—	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	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