FiniteDimension

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

Statistics

Metric	Count
Definitions `toHomeomorphOfFiniteDimensional`, `toAffineIsometryEquiv`, `piRing`, `toLinearIsometryEquiv`, `lipschitzExtensionConstant`	5
Theorems `coe_toHomeomorphOfFiniteDimensional`, `coe_toHomeomorphOfFiniteDimensional_symm`, `continuous_of_finiteDimensional`, `coe_toAffineIsometryEquiv`, `toAffineIsometryEquiv_apply`, `antilipschitzWith_of_finiteDimensional`, `continuous_of_finiteDimensional`, `lipschitzWith_of_finiteDimensional`, `closed_of_finiteDimensional`, `comp_summable`, `continuous_det`, `isOpen_injective`, `of_isCompact_closedBall`, `of_isCompact_closedBall₀`, `of_locallyCompactSpace`, `proper`, `proper_real`, `eq_one_or_finiteDimensional`, `eq_zero_or_finiteDimensional`, `exists_mem_frontier_infDist_compl_eq_dist`, `summable_iff`, `summable_iff_nat`, `eventually`, `coe_toLinearIsometryEquiv`, `toLinearIsometryEquiv_apply`, `exists_antilipschitzWith`, `injective_iff_antilipschitz`, `extend_finite_dimension`, `continuous_coe_repr`, `continuous_toMatrix`, `exists_opNNNorm_le`, `exists_opNorm_le`, `opNNNorm_le`, `opNorm_le`, `of_locallyCompactSpace`, `of_locallyCompact_module`, `norm`, `continuousOn_clm_apply`, `continuous_clm_apply`, `exists_mem_frontier_infDist_compl_eq_dist`, `exists_norm_le_le_norm_sub_of_finset`, `exists_seq_norm_le_one_le_norm_sub`, `exists_seq_norm_le_one_le_norm_sub'`, `instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace`, `instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional`, `isOpen_setOf_affineIndependent`, `isOpen_setOf_linearIndependent`, `isOpen_setOf_nat_le_rank`, `lipschitzExtensionConstant_def`, `lipschitzExtensionConstant_pos`, `summable_norm_iff`, `summable_norm_mul_geometric_of_norm_lt_one'`, `summable_of_isBigO'`, `summable_of_isBigO_nat'`, `summable_of_isEquivalent`, `summable_of_isEquivalent_nat`, `summable_of_sum_range_norm_le`	57
Total	62

AffineEquiv

Definitions

Name	Category	Theorems
`toHomeomorphOfFiniteDimensional` 📖	CompOp	2 math math: `coe_toHomeomorphOfFiniteDimensional_symm`, `coe_toHomeomorphOfFiniteDimensional`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toHomeomorphOfFiniteDimensional` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorphOfFiniteDimensional` `AffineEquiv` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `equivLike`	—	—
`coe_toHomeomorphOfFiniteDimensional_symm` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorphOfFiniteDimensional` `AffineEquiv` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `equivLike` `symm`	—	—
`continuous_of_finiteDimensional` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `AffineEquiv` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `EquivLike.toFunLike` `equivLike`	—	`AffineMap.continuous_of_finiteDimensional`

AffineIsometry

Definitions

Name	Category	Theorems
`toAffineIsometryEquiv` 📖	CompOp	2 math math: `coe_toAffineIsometryEquiv`, `toAffineIsometryEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toAffineIsometryEquiv` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	`DFunLike.coe` `AffineIsometryEquiv` `MetricSpace.toPseudoMetricSpace` `EquivLike.toFunLike` `AffineIsometryEquiv.instEquivLike` `toAffineIsometryEquiv` `AffineIsometry` `instFunLike`	—	—
`toAffineIsometryEquiv_apply` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	`DFunLike.coe` `AffineIsometryEquiv` `MetricSpace.toPseudoMetricSpace` `EquivLike.toFunLike` `AffineIsometryEquiv.instEquivLike` `toAffineIsometryEquiv` `AffineIsometry` `instFunLike`	—	—

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antilipschitzWith_of_finiteDimensional` 📖	mathematical	`DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `instFunLike`	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	—	`LinearMap.injective_iff_antilipschitz` `linear_injective_iff` `AntilipschitzWith.of_le_mul_dist` `dist_eq_norm_vsub` `linearMap_vsub` `ZeroHomClass.bound_of_antilipschitz` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`continuous_of_finiteDimensional` 📖	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`	—	`continuous_linear_iff` `instIsTopologicalAddTorsor_1` `LinearMap.continuous_of_finiteDimensional` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`lipschitzWith_of_finiteDimensional` 📖	mathematical	—	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `DFunLike.coe` `AffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `instFunLike`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `RingHomIsometric.ids` `LipschitzWith.of_dist_le_mul` `NormedAddTorsor.dist_eq_norm'` `linearMap_vsub` `ContinuousLinearMap.le_opNorm`

AffineSubspace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closed_of_finiteDimensional` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `SetLike.coe` `AffineSubspace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `instSetLike`	—	`isClosed_direction_iff` `instIsTopologicalAddTorsor_1` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Submodule.closed_of_finiteDimensional` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_summable` 📖	—	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	—	`Summable.of_norm` `comp_summable_norm` `Summable.norm`

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`piRing` 📖	CompOp	—

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_det` 📖	mathematical	—	`Continuous` `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` `topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `det` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `LinearMap.det_eq_det_toMatrix_of_finset` `Continuous.matrix_det` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `LinearMap.continuous_of_finiteDimensional` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `topologicalAddGroup` `continuousSMul` `RingHomSurjective.ids` `RingHomIsometric.ids` `IsBoundedSMul.continuousSMul` `instIsTopologicalAddGroupMatrix` `instContinuousSMulMatrix` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `instModuleFinite` `Module.Basis.finiteDimensional_of_finite` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `RingHomCompTriple.ids` `LinearMap.det_def` `continuous_const`
`isOpen_injective` 📖	mathematical	—	`IsOpen` `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` `topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `setOf` `DFunLike.coe` `funLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `isOpen_iff_eventually` `LinearMap.injective_iff_antilipschitz` `RingHomIsometric.ids` `eventually_nnnorm_sub_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Filter.mp_mem` `Filter.univ_mem'` `tsub_pos_of_lt` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `AntilipschitzWith.add_sub_lipschitzWith` `lipschitz`

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isCompact_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall`	`FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`of_isCompact_closedBall₀` `Metric.vadd_closedBall` `NormedAddGroup.to_isIsometricVAdd_left` `neg_add_cancel` `IsCompact.vadd` `IsIsometricVAdd.to_continuousConstVAdd`
`of_isCompact_closedBall₀` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule`	—	`exists_seq_norm_le_one_le_norm_sub` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.trans` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `NormedField.exists_norm_lt` `dist_zero_right` `norm_smul` `NormedSpace.toNormSMulClass` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `LT.lt.le` `norm_nonneg` `le_of_lt` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `IsUnit.div_mul_cancel` `LT.lt.ne'` `IsCompact.tendsto_subseq` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Tendsto.cauchySeq` `Metric.cauchySeq_iff'` `lt_irrefl` `mul_one` `dist_eq_norm` `mul_le_mul_of_nonneg_left` `ne_of_gt`
`of_locallyCompactSpace` 📖	mathematical	—	`FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Metric.exists_isCompact_closedBall` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `of_isCompact_closedBall₀`
`proper` 📖	mathematical	—	`ProperSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ProperSpace.of_locallyCompactSpace` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Pi.topologicalAddGroup` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `complete_of_proper` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Pi.t2Space` `finiteDimensional_pi'` `Finite.of_fintype` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `Module.finrank_fin_fun` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `AntilipschitzWith.properSpace` `RingHomIsometric.ids` `pi_properSpace` `ContinuousLinearEquiv.antilipschitz` `ContinuousLinearEquiv.continuous` `ContinuousLinearEquiv.surjective`
`proper_real` 📖	mathematical	—	`ProperSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`proper` `locallyCompact_of_proper` `instProperSpaceReal`

HasCompactMulSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_one_or_finiteDimensional` 📖	mathematical	`HasCompactMulSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Continuous`	`Pi.instOne` `FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`HasCompactSupport.eq_zero_or_finiteDimensional`

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_or_finiteDimensional` 📖	mathematical	`HasCompactSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Continuous`	`Pi.instZero` `FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule`	—	`FiniteDimensional.of_locallyCompactSpace` `eq_zero_or_locallyCompactSpace_of_addGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_frontier_infDist_compl_eq_dist` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`frontier` `Metric.infDist` `Compl.compl` `Set.instCompl` `Dist.dist` `PseudoMetricSpace.toDist`	—	`closure_eq_interior_union_frontier` `subset_closure` `Filter.HasBasis.mem_iff` `Metric.nhds_basis_closedBall` `mem_interior_iff_mem_nhds` `FiniteDimensional.of_isCompact_closedBall` `Real.instCompleteSpace` `of_isClosed_subset` `Metric.isClosed_closedBall` `exists_mem_frontier_infDist_compl_eq_dist` `ne_univ` `RealNormedSpace.noncompactSpace` `Metric.infDist_zero_of_mem_closure` `frontier_eq_closure_inter_closure` `dist_self`

IsEquivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`summable_iff` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.cofinite`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`summable_of_isEquivalent` `Asymptotics.IsEquivalent.symm`
`summable_iff_nat` 📖	mathematical	`Asymptotics.IsEquivalent` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.atTop` `Nat.instPreorder`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`summable_of_isEquivalent_nat` `Asymptotics.IsEquivalent.symm`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually` 📖	mathematical	`LinearIndependent` `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`	`Filter.Eventually` `nhds` `Pi.topologicalSpace`	—	`nonempty_fintype` `RingHomInvPair.ids` `AddMonoid.nat_smulCommClass'` `IsScalarTower.left` `LinearMap.exists_antilipschitzWith` `FiniteDimensional.finiteDimensional_pi'` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `tendsto_finset_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.norm` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.tendsto` `continuous_apply` `tendsto_const_nhds` `Filter.Eventually.mono` `Filter.Tendsto.eventually` `Finset.sum_congr` `sub_self` `norm_zero` `Finset.sum_const_zero` `gt_mem_nhds` `instOrderTopologyReal` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `NNReal.coe_lt_coe` `NNReal.coe_sum` `LinearMap.ker_eq_bot` `AntilipschitzWith.injective` `AntilipschitzWith.add_sub_lipschitzWith` `LipschitzWith.of_dist_le_mul` `RingHomCompTriple.ids` `LinearMap.sum_apply` `dist_eq_norm` `Finset.sum_mul` `norm_sum_le_of_le` `norm_smul` `NormedSpace.toNormSMulClass` `mul_comm` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_le_pi_norm` `norm_nonneg`

LinearIsometry

Definitions

Name	Category	Theorems
`toLinearIsometryEquiv` 📖	CompOp	2 math math: `coe_toLinearIsometryEquiv`, `toLinearIsometryEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toLinearIsometryEquiv` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `toLinearIsometryEquiv` `LinearIsometry` `instFunLike`	—	`RingHomInvPair.ids`
`toLinearIsometryEquiv_apply` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	`DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `toLinearIsometryEquiv` `LinearIsometry` `instFunLike`	—	`RingHomInvPair.ids`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_antilipschitzWith` 📖	mathematical	`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` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `Submodule.instBot`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `DFunLike.coe` `LinearMap` `instFunLike`	—	`subsingleton_or_nontrivial` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `AntilipschitzWith.of_subsingleton` `RingHomInvPair.ids` `RingHomSurjective.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `RingHomSurjective.invPair` `Submodule.topologicalAddGroup` `SMulMemClass.continuousSMul` `Submodule.smulMemClass` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `instT2SpaceSubtype` `ker_eq_bot` `IsScalarTower.left` `RingHomIsometric.ids` `ContinuousLinearEquiv.nnnorm_symm_pos` `ContinuousLinearEquiv.antilipschitz`
`injective_iff_antilipschitz` 📖	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` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`ker_eq_bot` `exists_antilipschitzWith` `AntilipschitzWith.injective`

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend_finite_dimension` 📖	mathematical	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`LipschitzWith` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `lipschitzExtensionConstant` `Set.EqOn`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Pi.t2Space` `Finite.of_fintype` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `RingHomIsometric.ids` `ContinuousLinearEquiv.lipschitz` `LipschitzWith.comp_lipschitzOnWith` `extend_pi` `LipschitzWith.weaken` `LipschitzWith.comp` `lipschitzExtensionConstant_def` `mul_assoc` `mul_le_mul'` `NNReal.mulLeftMono` `covariant_swap_mul_of_covariant_mul` `le_max_left` `le_rfl` `ContinuousLinearEquiv.symm_apply_apply`

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_coe_repr` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `repr`	—	`Module.Finite.of_basis` `LinearMap.continuous_of_finiteDimensional` `Pi.topologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RingHomInvPair.ids`
`continuous_toMatrix` 📖	mathematical	—	`Continuous` `Matrix` `Pi.topologicalSpace` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `toMatrix` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `AddCommGroup.toAddCommMonoid`	—	`Module.Finite.of_basis` `LinearMap.continuous_of_finiteDimensional` `Pi.topologicalAddGroup` `instContinuousSMulForall` `instIsTopologicalAddGroupMatrix` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instContinuousSMulMatrix` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Pi.t2Space` `FiniteDimensional.finiteDimensional_pi'` `RingHomInvPair.ids`
`exists_opNNNorm_le` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Preorder.toLE` `NNNorm.nnnorm` `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` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiringNNReal`	—	`nonempty_fintype` `RingHomIsometric.ids` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `LT.lt.trans_le` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `le_max_right` `LE.le.trans` `Finite.of_fintype` `opNNNorm_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `NNReal.instIsOrderedRing` `le_max_left` `zero_le` `NNReal.instCanonicallyOrderedAdd`
`exists_opNorm_le` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Norm.norm` `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.hasOpNorm` `Real.instMul`	—	`RingHomIsometric.ids` `exists_opNNNorm_le`
`opNNNorm_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `Module.Basis` `instFunLike`	`ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiringNNReal` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Fintype.card` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Pi.topologicalSpace` `SeminormedRing.toPseudoMetricSpace` `Pi.addCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.Function.module` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Pi.seminormedAddCommGroup` `Pi.normedSpace` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `equivFunL` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NormedSpace.toIsBoundedSMul` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`ContinuousLinearMap.opNNNorm_le_bound` `RingHomIsometric.ids` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `sum_equivFun` `Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `nnnorm_sum_le` `nnnorm_smul` `NormedSpace.toNormSMulClass` `Finset.sum_le_sum` `NNReal.addLeftMono` `mul_le_mul_right` `NNReal.mulLeftMono` `Finset.sum_mul` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `Pi.sum_nnnorm_apply_le_nnnorm` `nsmul_le_nsmul_right` `covariant_swap_add_of_covariant_add` `ContinuousLinearMap.le_opNNNorm` `smul_mul_assoc` `IsScalarTower.right` `mul_right_comm`
`opNorm_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `NormedAddCommGroup.toNorm` `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` `Module.Basis` `instFunLike`	`ContinuousLinearMap.hasOpNorm` `Real.instMul` `AddMonoid.toNatSMul` `Real.instAddMonoid` `Fintype.card` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Pi.topologicalSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Pi.addCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.Function.module` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Pi.seminormedAddCommGroup` `Pi.normedSpace` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `equivFunL` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NormedSpace.toIsBoundedSMul` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `nsmul_eq_mul` `RingHomIsometric.ids` `NNReal.coe_natCast` `NNReal.coe_le_coe` `opNNNorm_le`

ProperSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_locallyCompactSpace` 📖	mathematical	—	`ProperSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Metric.exists_isCompact_closedBall` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `NormedField.exists_one_lt_norm` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `norm_zero` `LE.le.not_gt` `zero_le_one` `Real.instZeroLEOneClass` `smul_closedBall'` `smul_zero` `norm_pow` `NormedDivisionRing.to_normOneClass` `IsCompact.smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.Tendsto.atTop_mul_const` `Real.instIsStrictOrderedRing` `tendsto_pow_atTop_atTop_of_one_lt` `AddGroup.existsAddOfLE` `Real.instArchimedean` `of_seq_closedBall` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Eventually.of_forall`
`of_locallyCompact_module` 📖	mathematical	—	`ProperSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField`	—	`exists_ne` `isClosedEmbedding_smul_left` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Topology.IsClosedEmbedding.locallyCompactSpace` `of_locallyCompactSpace`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm` 📖	mathematical	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	`Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`summable_norm_iff`

(root)

Definitions

Name	Category	Theorems
`lipschitzExtensionConstant` 📖	CompOp	3 math math: `lipschitzExtensionConstant_def`, `LipschitzOnWith.extend_finite_dimension`, `lipschitzExtensionConstant_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_clm_apply` 📖	mathematical	—	`ContinuousOn` `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.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `DFunLike.coe` `ContinuousLinearMap.funLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.comp_continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.continuous` `Module.finrank_fin_fun` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RingHomInvPair.ids` `IsBoundedSMul.continuousSMul` `Pi.topologicalAddGroup` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Pi.t2Space` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `RingHomCompTriple.ids` `ContinuousLinearEquiv.symm_comp_self` `ContinuousLinearEquiv.continuous` `continuousOn_pi`
`continuous_clm_apply` 📖	mathematical	—	`Continuous` `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.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `DFunLike.coe` `ContinuousLinearMap.funLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`exists_mem_frontier_infDist_compl_eq_dist` 📖	mathematical	`Set` `Set.instMembership`	`frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.infDist` `Compl.compl` `Set.instCompl` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Metric.exists_mem_closure_infDist_eq_dist` `FiniteDimensional.proper_real` `Set.nonempty_compl` `Metric.closedBall_infDist_compl_subset_closure` `Metric.mem_closedBall` `ge_of_eq` `dist_comm` `closure_compl`
`exists_norm_le_le_norm_sub_of_finset` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Norm.norm` `NormedField.toNorm` `NontriviallyNormedField.toNormedField` `FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Real.instLE` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Submodule.closed_of_finiteDimensional` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Module.Finite.of_fg` `Mathlib.Tactic.Contrapose.contrapose₂` `Submodule.ext` `riesz_lemma_of_norm_lt` `norm_neg` `neg_sub` `Submodule.subset_span`
`exists_seq_norm_le_one_le_norm_sub` 📖	mathematical	`FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Pairwise` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`NormedField.exists_one_lt_norm` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_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.sub_nonpos_of_le` `Real.instIsOrderedRing` `exists_seq_norm_le_one_le_norm_sub'` `LT.lt.trans`
`exists_seq_norm_le_one_le_norm_sub'` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Norm.norm` `NormedField.toNorm` `NontriviallyNormedField.toNormedField` `FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Real.instLE` `NormedAddCommGroup.toNorm` `Pairwise` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`norm_neg` `neg_sub` `exists_seq_of_forall_finset_exists'` `exists_norm_le_le_norm_sub_of_finset`
`instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace` 📖	mathematical	—	`ProperSpace` `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` `SetLike.instMembership` `Submodule.setLike` `Subtype.pseudoMetricSpace`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `proper_of_compact` `Finite.compactSpace` `Subtype.finite` `Finite.of_subsingleton` `ProperSpace.of_locallyCompact_module` `FiniteDimensional.of_locallyCompactSpace` `FiniteDimensional.proper` `IsScalarTower.left` `locallyCompact_of_proper` `FiniteDimensional.finiteDimensional_submodule`
`instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional` 📖	mathematical	—	`SecondCountableTopology` `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.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`RingHomIsometric.ids` `TopologicalSpace.exists_dense_seq` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `AddTorsor.nonempty` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `Module.Basis.exists_opNorm_le` `Finite.of_fintype` `Nat.instAtLeastTwoHAddOfNat` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `zero_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `norm_sub_rev` `dist_eq_norm` `mem_closure_iff_nhds_basis` `Metric.nhds_basis_ball` `le_of_lt` `Module.Basis.constrL_basis` `eq_div_iff` `two_ne_zero` `CharZero.NeZero.two` `mul_comm` `mul_assoc` `mul_div_cancel₀` `ne_of_gt` `dist_triangle` `Module.Basis.constrL.congr_simp` `dist_comm` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Metric.secondCountable_of_countable_discretization`
`isOpen_setOf_affineIndependent` 📖	mathematical	—	`IsOpen` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `setOf` `AffineIndependent` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor`	—	`isEmpty_or_nonempty` `isOpen_discrete` `Finite.instDiscreteTopology` `instT1SpaceForall` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Finite.of_fintype` `affineIndependent_iff_linearIndependent_vsub` `nonempty_fintype` `IsOpen.preimage` `continuous_pi` `Continuous.vsub` `instIsTopologicalAddTorsor_1` `continuous_apply` `isOpen_setOf_linearIndependent` `Subtype.finite`
`isOpen_setOf_linearIndependent` 📖	mathematical	—	`IsOpen` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `setOf` `LinearIndependent` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule`	—	`isOpen_iff_mem_nhds` `LinearIndependent.eventually`
`isOpen_setOf_nat_le_rank` 📖	mathematical	—	`IsOpen` `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.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `setOf` `Cardinal` `Cardinal.instLE` `Cardinal.instNatCast` `LinearMap.rank` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toLinearMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Set.setOf_exists` `isOpen_biUnion` `continuous_pi` `ContinuousLinearMap.continuous` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsOpen.preimage` `isOpen_setOf_linearIndependent` `Finite.of_fintype`
`lipschitzExtensionConstant_def` 📖	mathematical	—	`lipschitzExtensionConstant`	—	`Real.instCompleteSpace`
`lipschitzExtensionConstant_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `lipschitzExtensionConstant`	—	`Real.instCompleteSpace` `lipschitzExtensionConstant_def` `LT.lt.trans_le` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `le_max_right`
`summable_norm_iff` 📖	mathematical	—	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Summable.of_norm` `complete_of_proper` `FiniteDimensional.proper_real` `Summable.abs` `Real.instIsOrderedAddMonoid` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `Pi.summable` `Summable.of_norm_bounded` `summable_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `norm_norm` `pi_norm_le_iff_of_nonneg` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `norm_nonneg` `Finset.single_le_sum` `Finset.mem_univ` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `commRing_strongRankCondition` `Real.instNontrivial` `Module.Free.of_divisionRing` `ContinuousLinearEquiv.summable` `RingHomIsometric.ids` `Summable.mul_left` `ContinuousLinearEquiv.symm_apply_apply` `ContinuousLinearMap.le_opNorm`
`summable_norm_mul_geometric_of_norm_lt_one'` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instOne` `Asymptotics.IsBigO` `Filter.atTop` `Nat.instPreorder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `Monoid.toNatPow` `Nat.instMonoid`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional`	—	`exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `summable_of_isBigO_nat` `Real.instCompleteSpace` `Summable.norm` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `summable_geometric_of_lt_one` `LE.le.trans` `norm_nonneg` `LT.lt.le` `Asymptotics.IsBigOWith.isBigO` `Asymptotics.IsBigOWith.of_bound` `Filter.mp_mem` `eventually_norm_pow_le` `Filter.univ_mem'` `norm_mul` `norm_pow` `NormedDivisionRing.toNormMulClass` `norm_norm` `NormedDivisionRing.to_normOneClass` `CStarRing.norm_of_mem_unitary` `instCStarRingReal` `Real.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `one_mul` `Nat.cast_pow` `Asymptotics.IsBigO.mul` `Asymptotics.isBigO_norm_left` `Asymptotics.isBigO_norm_right` `Asymptotics.isBigO_refl` `Asymptotics.IsLittleO.isBigO` `isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt`
`summable_of_isBigO'` 📖	—	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.cofinite`	—	—	`summable_of_isBigO` `Summable.norm` `Asymptotics.IsBigO.norm_right`
`summable_of_isBigO_nat'` 📖	—	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional` `Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.atTop` `Nat.instPreorder`	—	—	`summable_of_isBigO_nat` `Summable.norm` `Asymptotics.IsBigO.norm_right`
`summable_of_isEquivalent` 📖	—	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional` `Asymptotics.IsEquivalent` `Filter.cofinite`	—	—	`Summable.trans_sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `summable_of_isBigO'` `complete_of_proper` `FiniteDimensional.proper_real` `Asymptotics.IsLittleO.isBigO` `Asymptotics.IsEquivalent.isLittleO`
`summable_of_isEquivalent_nat` 📖	—	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional` `Asymptotics.IsEquivalent` `Filter.atTop` `Nat.instPreorder`	—	—	`Summable.trans_sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `summable_of_isBigO_nat'` `complete_of_proper` `FiniteDimensional.proper_real` `Asymptotics.IsLittleO.isBigO` `Asymptotics.IsEquivalent.isLittleO`
`summable_of_sum_range_norm_le` 📖	mathematical	`Real` `Real.instLE` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Norm.norm` `NormedAddCommGroup.toNorm`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`summable_norm_iff` `summable_of_sum_range_le` `norm_nonneg`

---

← Back to Index