Documentation Verification Report

ApproximateUnit

📁 Source: Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

Statistics

Metric	Count
Definitions `approximateUnit`, `IsIncreasingApproximateUnit`	2
Theorems `monotoneOn_one_sub_one_add_inv`, `monotoneOn_one_sub_one_add_inv_real`, `directedOn_nonneg_ball`, `hasBasis_approximateUnit`, `increasingApproximateUnit`, `isBasis_nonneg_sections`, `nnnorm_sub_mul_self_le`, `norm_sub_mul_self_le`, `norm_sub_mul_self_le_of_inr`, `tendsto_mul_left_iff_tendsto_mul_right`, `tendsto_mul_right_of_forall_nonneg_tendsto`, `eventually_isSelfAdjoint`, `eventually_nnnorm`, `eventually_nonneg`, `eventually_norm`, `eventually_star_eq`, `toIsApproximateUnit`, `one_sub_one_add_inv`, `norm_cfcₙ_one_sub_one_add_inv_lt_one`	19
Total	21

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monotoneOn_one_sub_one_add_inv` 📖	mathematical	—	`MonotoneOn` `PartialOrder.toPreorder` `cfcₙ` `NNReal` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `instCommSemiringNNReal` `instNontrivialNNReal` `instStarRingNNReal` `instMetricSpaceNNReal` `NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `NonUnitalCStarAlgebra.toStarRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NNReal.instModuleOfReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `NonUnitalCStarAlgebra.toNormedSpace` `NNReal.instIsScalarTowerOfReal` `DistribMulAction.toMulAction` `Real.instMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `Module.toDistribMulAction` `Real.semiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `IsScalarTower.complexToReal` `NormedAddCommGroup.toAddCommGroup` `Complex` `Complex.instNormedField` `NonUnitalCStarAlgebra.toIsScalarTower` `NNReal.smulCommClass_left` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `Nonneg.instNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `NNReal.instSub` `instOneNNReal` `NNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Set.Ici`	—	`NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.complexToReal` `NonUnitalCStarAlgebra.toIsScalarTower` `NNReal.smulCommClass_left` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `Nonneg.instNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `Unitization.inr_le_iff` `IsSelfAdjoint.of_nonneg` `NonUnitalCStarAlgebra.toStarModule` `IsScalarTower.left` `Nonneg.instContinuousFunctionalCalculus` `Unitization.instStarOrderedRing` `IsSelfAdjoint.instContinuousFunctionalCalculus` `IsStarNormal.instContinuousFunctionalCalculus` `Unitization.nnreal_cfcₙ_eq_cfc_inr` `add_zero` `inv_one` `tsub_self` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `cfc_tsub` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CStarRing.instRegularNormedAlgebra` `NonUnitalCStarAlgebra.toCStarRing` `Unique.instSubsingleton` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `mul_one` `NNReal.addLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `continuousOn_const` `ContinuousOn.inv₀` `NNReal.instContinuousInv₀` `ContinuousOn.fun_add` `IsTopologicalSemiring.toContinuousAdd` `continuousOn_id'` `ne_of_gt` `add_pos_of_pos_of_nonneg` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `zero_le` `cfc_const_one` `cfc_comp'` `NNReal.instContinuousMap.UniqueHom` `continuousOn_id` `Set.forall_mem_image` `cfc_add` `cfc_id'` `Unitization.inr_nonneg_iff` `sub_le_sub_left` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `rpow_neg_one_eq_cfc_inv` `CStarAlgebra.rpow_neg_one_le_rpow_neg_one` `add_le_add_right` `isStrictlyPositive_add` `instZeroLEOneClass`
`monotoneOn_one_sub_one_add_inv_real` 📖	mathematical	—	`MonotoneOn` `PartialOrder.toPreorder` `cfcₙ` `Real` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `StarRing.toStarAddMonoid` `NonUnitalCStarAlgebra.toStarRing` `Real.instCommSemiring` `Real.instNontrivial` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `NonUnitalCStarAlgebra.toNormedSpace` `IsScalarTower.complexToReal` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `Complex` `Complex.instNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalCStarAlgebra.toIsScalarTower` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `Real.instSub` `Real.instOne` `Real.instInv` `Real.instAdd` `Set.Ici` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `IsScalarTower.complexToReal` `NonUnitalCStarAlgebra.toIsScalarTower` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `NNReal.instIsScalarTowerOfReal` `NNReal.smulCommClass_left` `Nonneg.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `cfcₙ_nnreal_eq_real` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `cfcₙ_congr` `NNReal.coe_sub` `Unique.instSubsingleton` `NNReal.instCanonicallyOrderedAdd` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `mul_one` `NNReal.addLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `sup_of_le_left` `monotoneOn_one_sub_one_add_inv`

CStarAlgebra

Definitions

Name	Category	Theorems
`approximateUnit` 📖	CompOp	2 math math: `increasingApproximateUnit`, `hasBasis_approximateUnit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directedOn_nonneg_ball` 📖	mathematical	—	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instInter` `setOf` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Metric.ball` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `Real` `Real.instOne`	—	`NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.complexToReal` `NonUnitalCStarAlgebra.toIsScalarTower` `NNReal.smulCommClass_left` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `Nonneg.instNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `instNonnegSpectrumClass'` `cfcₙ_id` `cfcₙ_congr` `Set.EqOn.mono` `lt_of_le_of_lt` `le_nnnorm_of_mem_quasispectrum` `Set.EqOn.symm` `Set.LeftInvOn.eqOn` `Set.InvOn.one_sub_one_add_inv` `cfcₙ_comp` `NNReal.instContinuousMapZero.UniqueHom` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousOn.sub` `NNReal.instContinuousSub` `continuousOn_const` `ContinuousOn.inv₀` `NNReal.instContinuousInv₀` `ContinuousOn.fun_add` `IsTopologicalSemiring.toContinuousAdd` `continuousOn_id'` `ne_of_gt` `add_pos_of_pos_of_nonneg` `NNReal.addLeftMono` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `zero_le` `NNReal.instCanonicallyOrderedAdd` `add_zero` `inv_one` `tsub_self` `NNReal.instOrderedSub` `LT.lt.ne'` `tsub_pos_of_lt` `ContinuousOn.fun_mul` `IsTopologicalSemiring.toContinuousMul` `MulZeroClass.zero_mul` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `cfcₙ_nonneg_of_predicate` `CFC.monotoneOn_one_sub_one_add_inv` `LE.le.trans` `dist_zero_right` `norm_cfcₙ_one_sub_one_add_inv_lt_one` `add_comm`
`hasBasis_approximateUnit` 📖	mathematical	—	`Filter.HasBasis` `approximateUnit` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Real` `Real.instLT` `Norm.norm` `NonUnitalNormedRing.toNorm` `Real.instOne` `Set` `Set.instInter` `setOf` `Metric.closedBall` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing`	—	`Filter.HasBasis.inf_principal` `isBasis_nonneg_sections` `Filter.IsBasis.hasBasis`
`increasingApproximateUnit` 📖	mathematical	—	`Filter.IsIncreasingApproximateUnit` `approximateUnit`	—	`tendsto_mul_left_iff_tendsto_mul_right` `Filter.HasBasis.eventually_iff` `hasBasis_approximateUnit` `LE.le.isSelfAdjoint` `LE.le.trans` `Filter.HasBasis.ex_mem` `Filter.HasBasis.neBot_iff` `le_rfl` `dist_zero_right` `LT.lt.le` `Filter.Eventually.filter_mono` `isBasis_nonneg_sections` `inf_le_left` `Filter.IsBasis.hasBasis` `norm_zero` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `inf_le_right`
`isBasis_nonneg_sections` 📖	mathematical	—	`Filter.IsBasis` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Real` `Real.instLT` `Norm.norm` `NonUnitalNormedRing.toNorm` `Real.instOne` `setOf`	—	`norm_zero` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `dist_zero_right` `LE.le.trans` `directedOn_nonneg_ball`
`nnnorm_sub_mul_self_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `toNormedRing` `Set` `Set.instMembership` `Set.Icc` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NNReal` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `toNonUnitalCStarAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `toStarRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal`	—	—	`one_mul` `NNReal.sqrt_sq` `NNReal.le_sqrt_iff_sq_le` `sub_mul` `sq` `CStarRing.nnnorm_star_mul_self` `toCStarRing` `StarMul.star_mul` `star_sub` `star_one` `LE.le.trans` `Set.sub_mem_Icc_zero_iff_right` `StarOrderedRing.toIsOrderedAddMonoid` `LE.le.star_eq` `mul_assoc` `nnnorm_le_nnnorm_of_nonneg_of_le` `star_left_conjugate_nonneg` `pow_nonneg` `star_left_conjugate_le_conjugate` `Nat.instAtLeastTwoHAddOfNat` `pow_one` `pow_antitone` `one_le_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `sub_le_sub_left` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `covariant_swap_add_of_covariant_add`
`norm_sub_mul_self_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `toNormedRing` `Set` `Set.instMembership` `Set.Icc` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real` `Real.instLE` `Real.instZero` `Norm.norm` `NormedRing.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `toStarRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `toNonUnitalCStarAlgebra` `Monoid.toNatPow` `Real.instMonoid`	—	—	`nnnorm_sub_mul_self_le`
`norm_sub_mul_self_le_of_inr` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Real` `Real.instLE` `Norm.norm` `NonUnitalNormedRing.toNorm` `Real.instOne` `Real.instZero` `Unitization` `Complex` `NormedRing.toNorm` `Unitization.instNormedRing` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NonUnitalCStarAlgebra.toNormedSpace` `NonUnitalCStarAlgebra.toIsScalarTower` `NonUnitalCStarAlgebra.toSMulCommClass` `CStarRing.instRegularNormedAlgebra` `NonUnitalCStarAlgebra.toStarRing` `NonUnitalCStarAlgebra.toCStarRing` `Unitization.instMul` `Complex.instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `Star.star` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `instCommCStarAlgebraComplex` `StarRing.toStarAddMonoid` `Complex.instStarRing` `Unitization.inr` `Complex.instZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Unitization.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Complex.instNormedAddCommGroup` `Unitization.instOne` `Complex.instOne` `Monoid.toNatPow` `Real.instMonoid`	—	—	`NonUnitalCStarAlgebra.toIsScalarTower` `NonUnitalCStarAlgebra.toSMulCommClass` `CStarRing.instRegularNormedAlgebra` `NonUnitalCStarAlgebra.toCStarRing` `Unitization.norm_inr` `Unitization.inr_sub` `Unitization.inr_mul` `norm_sub_mul_self_le` `Unitization.instStarOrderedRing` `Unitization.inr_nonneg_iff` `LE.le.trans` `Set.mem_Icc` `Unitization.inr_le_iff` `LE.le.isSelfAdjoint` `norm_le_one_iff_of_nonneg`
`tendsto_mul_left_iff_tendsto_mul_right` 📖	mathematical	`Filter.Eventually` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `StarRing.toStarAddMonoid` `NonUnitalCStarAlgebra.toStarRing`	`Filter.Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing`	—	`Filter.Tendsto.congr'` `Filter.Tendsto.comp` `Continuous.tendsto` `ContinuousStar.continuous_star` `NormedStarGroup.to_continuousStar` `CStarRing.to_normedStarGroup` `NonUnitalCStarAlgebra.toCStarRing` `star_star` `Filter.mp_mem` `Filter.univ_mem'` `StarMul.star_mul` `IsSelfAdjoint.star_eq`
`tendsto_mul_right_of_forall_nonneg_tendsto` 📖	—	`Filter.Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing`	—	—	`Submodule.mem_span_set'` `span_nonneg_inter_unitBall` `Finset.mul_sum` `tendsto_finset_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `mul_smul_comm` `NonUnitalCStarAlgebra.toSMulCommClass` `Filter.Tendsto.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `tendsto_const_nhds` `dist_zero_right`

Filter

Definitions

Name	Category	Theorems
`IsIncreasingApproximateUnit` 📖	CompData	1 math math: `CStarAlgebra.increasingApproximateUnit`

Filter.IsIncreasingApproximateUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_isSelfAdjoint` 📖	mathematical	`Filter.IsIncreasingApproximateUnit`	`Filter.Eventually` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `StarRing.toStarAddMonoid` `NonUnitalCStarAlgebra.toStarRing`	—	`Filter.Eventually.mp` `eventually_nonneg` `Filter.Eventually.of_forall` `IsSelfAdjoint.of_nonneg`
`eventually_nnnorm` 📖	mathematical	`Filter.IsIncreasingApproximateUnit`	`Filter.Eventually` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `instOneNNReal`	—	`eventually_norm`
`eventually_nonneg` 📖	mathematical	`Filter.IsIncreasingApproximateUnit`	`Filter.Eventually` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing`	—	—
`eventually_norm` 📖	mathematical	`Filter.IsIncreasingApproximateUnit`	`Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Real.instOne`	—	—
`eventually_star_eq` 📖	mathematical	`Filter.IsIncreasingApproximateUnit`	`Filter.Eventually` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `StarRing.toStarAddMonoid` `NonUnitalCStarAlgebra.toStarRing`	—	`Filter.Eventually.mp` `eventually_isSelfAdjoint` `Filter.Eventually.of_forall` `IsSelfAdjoint.star_eq`
`toIsApproximateUnit` 📖	mathematical	`Filter.IsIncreasingApproximateUnit`	`Filter.IsApproximateUnit` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing`	—	—

Set.InvOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_sub_one_add_inv` 📖	mathematical	—	`Set.InvOn` `NNReal` `NNReal.instSub` `instOneNNReal` `NNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Distrib.toMul` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal`	—	`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.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `add_pos_of_pos_of_nonneg` `NNReal.addLeftMono` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `mul_tsub` `NNReal.instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `mul_inv_cancel₀` `Unique.instSubsingleton` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `add_tsub_cancel_left` `tsub_pos_of_lt` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `tsub_add_cancel_of_le` `StarOrderedRing.toExistsAddOfLE` `NNReal.instStarOrderedRing` `LT.lt.le` `mul_assoc` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `add_tsub_cancel_right`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_cfcₙ_one_sub_one_add_inv_lt_one` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `cfcₙ` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `instCommSemiringNNReal` `instNontrivialNNReal` `instStarRingNNReal` `instMetricSpaceNNReal` `NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `NonUnitalCStarAlgebra.toStarRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NNReal.instModuleOfReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `NonUnitalCStarAlgebra.toNormedSpace` `NNReal.instIsScalarTowerOfReal` `DistribMulAction.toMulAction` `Real.instMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `Module.toDistribMulAction` `Real.semiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `IsScalarTower.complexToReal` `NormedAddCommGroup.toAddCommGroup` `Complex` `Complex.instNormedField` `NonUnitalCStarAlgebra.toIsScalarTower` `NNReal.smulCommClass_left` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `Nonneg.instNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `NNReal.instSub` `instOneNNReal` `NNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real.instOne`	—	`nnnorm_cfcₙ_nnreal_lt` `IsScalarTower.complexToReal` `NonUnitalCStarAlgebra.toIsScalarTower` `SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `tsub_lt_self` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `zero_lt_one` `instZeroLEOneClass` `NNReal.instStarOrderedRing` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `add_pos_of_pos_of_nonneg` `NNReal.addLeftMono` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `zero_le`

---

← Back to Index