Documentation Verification Report

PosPart

📁 Source: Mathlib/Analysis/CStarAlgebra/SpecialFunctions/PosPart.lean

Statistics

Metric	Count
Definitions `PosPart`	1
Theorems `exists_sum_four_nonneg`, `span_nonneg_inter_ball`, `span_nonneg_inter_closedBall`, `span_nonneg_inter_unitBall`, `span_nonneg_inter_unitClosedBall`	5
Total	6

CStarAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_sum_four_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Real` `Real.instLE` `Norm.norm` `NonUnitalNormedRing.toNorm` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `Finset.univ` `Fin.fintype` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `Monoid.toNatPow` `Complex.I`	—	`SMulCommClass.complexToReal` `NonUnitalCStarAlgebra.toSMulCommClass` `IsScalarTower.complexToReal` `NonUnitalCStarAlgebra.toIsScalarTower` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `instTrivialStarReal` `StarModule.complexToReal` `NonUnitalCStarAlgebra.toStarModule` `Fintype.complete` `CFC.posPart_nonneg` `LE.le.trans` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus` `norm_posPart_le` `realPart.norm_le` `CStarRing.to_normedStarGroup` `NonUnitalCStarAlgebra.toCStarRing` `imaginaryPart.norm_le` `CFC.negPart_nonneg` `norm_negPart_le` `linear_combination_nonneg` `Fin.sum_univ_four` `Complex.I_sq` `Complex.I_pow_three` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `add_zero` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `eq_intCast` `Int.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Int.cast_neg` `Mathlib.Tactic.Ring.neg_congr` `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_one` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.neg_mul`
`span_nonneg_inter_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Submodule.span` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `Set` `Set.instInter` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Metric.ball` `Top.top` `Submodule` `Submodule.instTop`	—	`eq_top_iff` `Nat.instAtLeastTwoHAddOfNat` `span_nonneg_inter_closedBall` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Submodule.span_mono` `Set.inter_subset_inter` `subset_refl` `Set.instReflSubset` `Metric.closedBall_subset_ball` `half_lt_self`
`span_nonneg_inter_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Submodule.span` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `Set` `Set.instInter` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Metric.closedBall` `Top.top` `Submodule` `Submodule.instTop`	—	`eq_top_iff` `span_nonneg` `NonUnitalCStarAlgebra.toSMulCommClass` `NonUnitalCStarAlgebra.toIsScalarTower` `NonUnitalCStarAlgebra.toStarModule` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `Submodule.span_le` `eq_zero_or_norm_pos` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `inv_smul_smul₀` `Nat.cast_zero` `ne_of_gt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Submodule.smul_mem` `Submodule.subset_span` `Set.mem_inter` `smul_nonneg` `IsOrderedModule.toPosSMulMono` `instIsOrderedModule` `Real.instStarOrderedRing` `StarModule.complexToReal` `IsScalarTower.complexToReal` `SMulCommClass.complexToReal` `le_of_lt` `Complex.ofReal_inv` `SemigroupAction.mul_smul` `dist_zero_right` `norm_smul` `NormedSpace.toNormSMulClass` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_inv` `Complex.norm_real` `norm_norm` `inv_mul_cancel₀` `LT.lt.ne'` `mul_one`
`span_nonneg_inter_unitBall` 📖	mathematical	—	`Submodule.span` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `Set` `Set.instInter` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Metric.ball` `Real` `Real.instOne` `Top.top` `Submodule` `Submodule.instTop`	—	`span_nonneg_inter_ball` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`span_nonneg_inter_unitClosedBall` 📖	mathematical	—	`Submodule.span` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `Set` `Set.instInter` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Metric.closedBall` `Real` `Real.instOne` `Top.top` `Submodule` `Submodule.instTop`	—	`span_nonneg_inter_closedBall` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`

(root)

Definitions

Name	Category	Theorems
`PosPart` 📖	CompData	—

---

← Back to Index