Banach

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

Statistics

Metric	Count
Definitions ofBijective, toNonlinearRightInverse, NonlinearRightInverse, nnnorm, toFun, coprodSubtypeLEquivOfIsCompl, equivRange, instCoeFunNonlinearRightInverseForall, nonlinearRightInverseOfSurjective, ofIsClosedGraph, ofSeqClosedGraph, toContinuousLinearEquivOfContinuous, instInhabitedNonlinearRightInverseToContinuousLinearMap	13
Theorems isOpenMap, completeSpace_range_clm, coeFn_ofBijective, coe_ofBijective, ofBijective_apply_symm_apply, ofBijective_symm_apply_apply, bound', right_inv, right_inv', antilipschitz_of_injective_of_isClosed_range, bijective_iff_dense_range_and_antilipschitz, closed_complemented_range_of_isCompl_of_ker_eq_bot, closed_range_of_antilipschitz, closure_preimage, coeFn_ofIsClosedGraph, coeFn_ofSeqClosedGraph, coe_equivRange, coe_linearMap_equivRange, coe_ofIsClosedGraph, coe_ofSeqClosedGraph, equivRange_symm_apply, equivRange_symm_toLinearEquiv, exists_approx_preimage_norm_le, exists_nonlinearRightInverse_of_surjective, exists_preimage_norm_le, frontier_preimage, interior_preimage, isClosed_range_iff_antilipschitz_of_injective, isOpenMap, isQuotientMap, isUnit_iff_bijective, isUnit_iff_isUnit_toLinearMap, nonlinearRightInverseOfSurjective_def, nonlinearRightInverseOfSurjective_nnnorm_pos, range_eq_map_coprodSubtypeLEquivOfIsCompl, coeFn_toContinuousLinearEquivOfContinuous, coeFn_toContinuousLinearEquivOfContinuous_symm, continuous_symm, continuous_of_isClosed_graph, continuous_of_seq_closed_graph	40
Total	53

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenMap 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace DFunLike.coe AffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor instFunLike	IsOpenMap	—	isOpenMap_linear_iff instIsTopologicalAddTorsor_1 ContinuousLinearMap.isOpenMap continuous_linear_iff RingHomInvPair.ids RingHomIsometric.ids linear_surjective_iff

AntilipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completeSpace_range_clm 📖	mathematical	AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace DFunLike.coe ContinuousLinearMap 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 ContinuousLinearMap.funLike	CompleteSpace Submodule SetLike.instMembership Submodule.setLike LinearMap.range RingHomSurjective.invPair ContinuousLinearMap.toLinearMap instUniformSpaceSubtype	—	IsClosed.completeSpace_coe RingHomSurjective.invPair isClosed_range ContinuousLinearMap.uniformContinuous SeminormedAddCommGroup.to_isUniformAddGroup

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
ofBijective 📖	CompOp	4 math math: coeFn_ofBijective, ofBijective_symm_apply_apply, coe_ofBijective, ofBijective_apply_symm_apply
toNonlinearRightInverse 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_ofBijective 📖	mathematical	LinearMap.ker 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 ContinuousLinearMap.toLinearMap Bot.bot Submodule Submodule.instBot LinearMap.range RingHomSurjective.invPair Top.top Submodule.instTop	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike ofBijective ContinuousLinearMap ContinuousLinearMap.funLike	—	RingHomSurjective.invPair
coe_ofBijective 📖	mathematical	LinearMap.ker 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 ContinuousLinearMap.toLinearMap Bot.bot Submodule Submodule.instBot LinearMap.range RingHomSurjective.invPair Top.top Submodule.instTop	toContinuousLinearMap ofBijective	—	RingHomSurjective.invPair ContinuousLinearMap.ext
ofBijective_apply_symm_apply 📖	mathematical	LinearMap.ker 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 ContinuousLinearMap.toLinearMap Bot.bot Submodule Submodule.instBot LinearMap.range RingHomSurjective.invPair Top.top Submodule.instTop	DFunLike.coe ContinuousLinearMap ContinuousLinearMap.funLike ContinuousLinearEquiv EquivLike.toFunLike equivLike symm ofBijective	—	RingHomSurjective.invPair apply_symm_apply
ofBijective_symm_apply_apply 📖	mathematical	LinearMap.ker 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 ContinuousLinearMap.toLinearMap Bot.bot Submodule Submodule.instBot LinearMap.range RingHomSurjective.invPair Top.top Submodule.instTop	DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike symm ofBijective ContinuousLinearMap ContinuousLinearMap.funLike	—	RingHomSurjective.invPair symm_apply_apply

ContinuousLinearMap

Definitions

Name	Category	Theorems
NonlinearRightInverse 📖	CompData	1 math math: nonlinearRightInverseOfSurjective_def
coprodSubtypeLEquivOfIsCompl 📖	CompOp	1 math math: range_eq_map_coprodSubtypeLEquivOfIsCompl
equivRange 📖	CompOp	4 math math: coe_equivRange, equivRange_symm_apply, equivRange_symm_toLinearEquiv, coe_linearMap_equivRange
instCoeFunNonlinearRightInverseForall 📖	CompOp	—
nonlinearRightInverseOfSurjective 📖	CompOp	2 math math: nonlinearRightInverseOfSurjective_def, nonlinearRightInverseOfSurjective_nnnorm_pos
ofIsClosedGraph 📖	CompOp	2 math math: coe_ofIsClosedGraph, coeFn_ofIsClosedGraph
ofSeqClosedGraph 📖	CompOp	2 math math: coe_ofSeqClosedGraph, coeFn_ofSeqClosedGraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz_of_injective_of_isClosed_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 funLike	AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	RingHomSurjective.invPair RingHomInvPair.ids IsScalarTower.left RingHomIsometric.ids AntilipschitzWith.comp AntilipschitzWith.subtype_coe ContinuousLinearEquiv.antilipschitz
bijective_iff_dense_range_and_antilipschitz 📖	mathematical	—	Function.Bijective DFunLike.coe ContinuousLinearMap 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 funLike Submodule.topologicalClosure UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup LinearMap.range RingHomSurjective.invPair toLinearMap Top.top Submodule Submodule.instTop AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomSurjective.invPair Dense.closure_eq Function.Surjective.denseRange ContinuousLinearEquiv.antilipschitz AntilipschitzWith.injective coe_coe LinearMap.range_eq_top closed_range_of_antilipschitz
closed_complemented_range_of_isCompl_of_ker_eq_bot 📖	mathematical	IsCompl Submodule 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 Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids toLinearMap LinearMap.ker Bot.bot Submodule.instBot	IsClosed SetLike.coe Submodule.setLike	—	RingHomSurjective.ids RingHomInvPair.ids IsClosed.completeSpace_coe range_eq_map_coprodSubtypeLEquivOfIsCompl Homeomorph.isClosed_image IsClosed.prod isClosed_univ isClosed_singleton Subtype.t1Space T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
closed_range_of_antilipschitz 📖	mathematical	AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace DFunLike.coe ContinuousLinearMap 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 funLike	Submodule.topologicalClosure UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup LinearMap.range RingHomSurjective.invPair toLinearMap	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomSurjective.invPair SetLike.ext'_iff IsClosed.closure_eq AntilipschitzWith.isClosed_range uniformContinuous SeminormedAddCommGroup.to_isUniformAddGroup
closure_preimage 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	closure Set.preimage	—	IsOpenMap.preimage_closure_eq_closure_preimage isOpenMap continuous
coeFn_ofIsClosedGraph 📖	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 funLike ofIsClosedGraph LinearMap LinearMap.instFunLike	—	—
coeFn_ofSeqClosedGraph 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule LinearMap.instFunLike	ContinuousLinearMap funLike ofSeqClosedGraph	—	—
coe_equivRange 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	ContinuousLinearEquiv Submodule SetLike.instMembership Submodule.setLike LinearMap.range RingHomSurjective.invPair toLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module EquivLike.toFunLike ContinuousLinearEquiv.equivLike equivRange rangeRestrict	—	RingHomSurjective.invPair
coe_linearMap_equivRange 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	ContinuousLinearEquiv.toContinuousLinearMap Submodule SetLike.instMembership Submodule.setLike LinearMap.range RingHomSurjective.invPair toLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module equivRange rangeRestrict	—	RingHomSurjective.invPair
coe_ofIsClosedGraph 📖	mathematical	—	toLinearMap 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 ofIsClosedGraph	—	LinearMap.ext
coe_ofSeqClosedGraph 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule LinearMap.instFunLike	toLinearMap ofSeqClosedGraph	—	LinearMap.ext
equivRange_symm_apply 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	ContinuousLinearEquiv Submodule SetLike.instMembership Submodule.setLike LinearMap.range RingHomSurjective.invPair toLinearMap instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm equivRange	—	RingHomSurjective.invPair
equivRange_symm_toLinearEquiv 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	LinearEquiv.symm Submodule SetLike.instMembership Submodule.setLike LinearMap.range RingHomSurjective.invPair toLinearMap Submodule.addCommMonoid Submodule.module ContinuousLinearEquiv.toLinearEquiv instTopologicalSpaceSubtype equivRange LinearEquiv.ofInjective	—	RingHomSurjective.invPair
exists_approx_preimage_norm_le 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	Real Real.instLE Real.instZero Dist.dist PseudoMetricSpace.toDist Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Norm.norm NormedAddCommGroup.toNorm	—	Set.Subset.antisymm Set.subset_univ exists_nat_gt Real.instIsStrictOrderedRing Real.instArchimedean Set.mem_iUnion subset_closure Set.mem_image Metric.mem_ball dist_eq_norm sub_zero nonempty_interior_of_iUnion_of_closed BaireSpace.of_completelyPseudoMetrizable TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable EMetric.instIsCountablyGeneratedUniformity T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity AddTorsor.nonempty instCountableNat isClosed_closure Nat.instAtLeastTwoHAddOfNat NormedField.exists_one_lt_norm mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE div_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_trans Nat.cast_one Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass eq_or_ne dist_zero_right one_div norm_zero MulZeroClass.mul_zero inv_div map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass RingHomIsometric.norm_map rescale_to_shell half_pos norm_pos_iff add_sub_cancel_left lt_of_le_of_lt LT.lt.le half_lt_self Metric.mem_closure_iff dist_self map_sub Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg norm_sub_le map_smulₛₗ inv_mul_cancel₀ one_smul map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHom.id_apply SemigroupAction.mul_smul smul_sub norm_smul NormedSpace.toNormSMulClass norm_inv mul_le_mul_of_nonneg_left Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false IsStrictOrderedRing.toCharZero Nat.cast_zero Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 mul_le_mul IsOrderedRing.toMulPosMono le_trans add_le_add covariant_swap_add_of_covariant_add norm_nonneg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.isNat_mul
exists_nonlinearRightInverse_of_surjective 📖	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 RingHomSurjective.invPair toLinearMap Top.top Submodule Submodule.instTop	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal NonlinearRightInverse.nnnorm	—	RingHomSurjective.invPair LT.lt.le GT.gt.lt exists_preimage_norm_le LinearMap.range_eq_top
exists_preimage_norm_le 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	Real Real.instLT Real.instZero Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul	—	Nat.instAtLeastTwoHAddOfNat exists_approx_preimage_norm_le dist_eq_norm dist_comm lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toCharZero one_div pow_zero one_mul Function.iterate_succ' le_trans pow_succ' mul_assoc mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Summable.of_nonneg_of_le norm_nonneg Summable.mul_right IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal summable_geometric_of_lt_one Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Summable.of_norm norm_tsum_le_tsum_norm Summable.tsum_le_tsum OrderTopology.to_orderClosedTopology instOrderTopologyReal SummationFilter.instNeBotUnconditional summable_geometric_two tsum_mul_right TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace tsum_geometric_two le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono map_zero sub_self Finset.sum_range_succ map_add Function.iterate_succ_apply' sub_add HasSum.tendsto_sum_nat Summable.hasSum Filter.Tendsto.comp Continuous.tendsto continuous Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup tendsto_const_nhds tendsto_iff_norm_sub_tendsto_zero sub_zero squeeze_zero MulZeroClass.zero_mul Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul tendsto_pow_atTop_nhds_zero_of_lt_one AddGroup.existsAddOfLE Real.instArchimedean Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat tendsto_nhds_unique Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
frontier_preimage 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	frontier Set.preimage	—	IsOpenMap.preimage_frontier_eq_frontier_preimage isOpenMap continuous
interior_preimage 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	interior Set.preimage	—	IsOpenMap.preimage_interior_eq_interior_preimage isOpenMap continuous
isClosed_range_iff_antilipschitz_of_injective 📖	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 funLike	IsClosed Set.range AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	antilipschitz_of_injective_of_isClosed_range AntilipschitzWith.isClosed_range uniformContinuous SeminormedAddCommGroup.to_isUniformAddGroup
isOpenMap 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	IsOpenMap	—	exists_preimage_norm_le Metric.isOpen_iff div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing map_add add_sub_cancel dist_self_add_left mul_lt_mul_of_pos_left dist_eq_norm Metric.mem_ball mul_div_cancel₀ ne_of_gt Set.mem_image_of_mem
isQuotientMap 📖	mathematical	DFunLike.coe ContinuousLinearMap 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 funLike	Topology.IsQuotientMap	—	IsOpenMap.isQuotientMap isOpenMap continuous
isUnit_iff_bijective 📖	mathematical	—	IsUnit 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 MonoidWithZero.toMonoid monoidWithZero Function.Bijective DFunLike.coe funLike	—	ContinuousLinearEquiv.bijective RingHomInvPair.ids RingHomIsometric.ids RingHomSurjective.invPair
isUnit_iff_isUnit_toLinearMap 📖	mathematical	—	IsUnit 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 MonoidWithZero.toMonoid monoidWithZero LinearMap Module.End.instMonoid toLinearMap	—	isUnit_iff_bijective Module.End.isUnit_iff
nonlinearRightInverseOfSurjective_def 📖	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 toLinearMap Top.top Submodule Submodule.instTop	nonlinearRightInverseOfSurjective NonlinearRightInverse NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal NonlinearRightInverse.nnnorm exists_nonlinearRightInverse_of_surjective	—	exists_nonlinearRightInverse_of_surjective RingHomSurjective.invPair
nonlinearRightInverseOfSurjective_nnnorm_pos 📖	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 RingHomSurjective.invPair toLinearMap Top.top Submodule Submodule.instTop	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal NonlinearRightInverse.nnnorm nonlinearRightInverseOfSurjective	—	RingHomSurjective.invPair exists_nonlinearRightInverse_of_surjective nonlinearRightInverseOfSurjective_def
range_eq_map_coprodSubtypeLEquivOfIsCompl 📖	mathematical	IsCompl Submodule 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 Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids toLinearMap LinearMap.ker Bot.bot Submodule.instBot	Submodule.map SetLike.instMembership Submodule.setLike Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module instTopologicalSpaceProd instTopologicalSpaceSubtype ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids coprodSubtypeLEquivOfIsCompl Submodule.prod Top.top Submodule.instTop	—	RingHomSurjective.ids RingHomInvPair.ids coprodSubtypeLEquivOfIsCompl.eq_1 ContinuousLinearEquiv.coe_ofBijective coe_coprod LinearMap.coprod_map_prod Submodule.map_bot sup_bot_eq Submodule.map_top

ContinuousLinearMap.NonlinearRightInverse

Definitions

Name	Category	Theorems
nnnorm 📖	CompOp	6 math math: ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse, ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective, bound, ContinuousLinearMap.nonlinearRightInverseOfSurjective_def, ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos, bound'
toFun 📖	CompOp	4 math math: bound, right_inv, right_inv', bound'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound' 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm toFun Real.instMul NNReal.toReal nnnorm	—	—
right_inv 📖	mathematical	—	DFunLike.coe ContinuousLinearMap 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 ContinuousLinearMap.funLike toFun	—	right_inv'
right_inv' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap 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 ContinuousLinearMap.funLike toFun	—	—

LinearEquiv

Definitions

Name	Category	Theorems
toContinuousLinearEquivOfContinuous 📖	CompOp	2 math math: coeFn_toContinuousLinearEquivOfContinuous, coeFn_toContinuousLinearEquivOfContinuous_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_toContinuousLinearEquivOfContinuous 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	ContinuousLinearEquiv ContinuousLinearEquiv.equivLike toContinuousLinearEquivOfContinuous	—	—
coeFn_toContinuousLinearEquivOfContinuous_symm 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	ContinuousLinearEquiv ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm toContinuousLinearEquivOfContinuous symm	—	—
continuous_symm 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	symm	—	continuous_def image_eq_preimage_symm coe_coe ContinuousLinearMap.isOpenMap surjective

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_of_isClosed_graph 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike	—	RingHomInvPair.ids RingHomSurjective.invPair RingHomCompTriple.ids RingHomSurjective.ids graph_eq_range_prod Prod.isScalarTower IsScalarTower.left RingHomIsometric.ids completeSpace_coe_iff_isComplete IsClosed.isComplete CompleteSpace.prod Continuous.fst continuous_subtype_val Continuous.snd Continuous.comp ContinuousLinearEquiv.continuous
continuous_of_seq_closed_graph 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike	Continuous	—	continuous_of_isClosed_graph IsSeqClosed.isClosed FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.instFirstCountableTopologyProd TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Filter.Tendsto.comp Continuous.tendsto continuous_fst continuous_snd

(root)

Definitions

Name	Category	Theorems
instInhabitedNonlinearRightInverseToContinuousLinearMap 📖	CompOp	—

---

← Back to Index