Notation

📁 Source: Mathlib/Algebra/Notation.lean

Statistics

Metric	Count
Definitions LeOnePart, leOnePart, NegPart, negPart, OneLePart, oneLePart, posPart, «term_⁺», «term_⁺ᵐ», «term_⁻», «term_⁻ᵐ»	11
Theorems	0
Total	11

LeOnePart

Definitions

Name	Category	Theorems
leOnePart 📖	CompOp	39 math math: oneLePart_leOnePart_injective, leOnePart_eq_inv_inf_one, leOnePart_le_one, leOnePart_of_one_le, leOnePart_div_oneLePart, leOnePart_eq_one', leOnePart_of_le_one, leOnePart_lt, leOnePart_le_one', one_lt_ltOnePart, oneLePart_inv, oneLePart_inf_leOnePart_eq_one, inv_le_leOnePart, leOnePart_eq_ite_lt, Pi.leOnePart_apply, leOnePart_eq_one, leOnePart_inv, leOnePart_max, Pi.leOnePart_def, leOnePart_one, leOnePart_mul_oneLePart, div_mabs_eq_inv_leOnePart_sq, measurable_leOnePart, one_lt_leOnePart, oneLePart_mul_leOnePart, leOnePart_min, one_le_leOnePart, leOnePart_eq_inv, le_iff_oneLePart_leOnePart, leOnePart_eq_ite, leOnePart_def, one_lt_leOnePart_iff, oneLePart_leOnePart_inj, leOnePart_eq_inv', mabs_div_eq_leOnePart_sq, oneLePart_div_leOnePart, Measurable.leOnePart, one_lt_ltOnePart_iff, leOnePart_anti

NegPart

Definitions

Name	Category	Theorems
negPart 📖	CompOp	76 math math: negPart_nonpos, Measurable.negPart, CFC.posPart_smul_of_nonpos, CFC.negPart_eq_zero_of_not_isSelfAdjoint, negPart_eq_zero', posPart_negPart_inj, negPart_eq_neg', CFC.negPart_mul_posPart, Pi.negPart_apply, negPart_sub_posPart, CFC.negPart_algebraMap, negPart_anti, negPart_max, ValueDistribution.logCounting_top, CFC.negPart_smul_of_nonpos, negPart_pos_iff, le_iff_posPart_negPart, CFC.posPart_sub_negPart, CStarAlgebra.nonneg_iff_isSelfAdjoint_and_negPart_eq_zero, CFC.posPart_mul_negPart, CFC.negPart_eq_neg, CFC.negPart_nonneg, CFC.negPart_eq_zero_iff, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right, CFC.negPart_zero, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left, CStarAlgebra.linear_combination_nonneg, negPart_eq_ite, posPart_sub_negPart, negPart_def, IsSelfAdjoint.norm_eq_max_norm_posPart_negPart, CFC.posPart_add_negPart, negPart_of_nonneg, Function.locallyFinsuppWithin.negPart_add, negPart_lt, CFC.negPart_one, lipschitzWith_negPart, Pi.negPart_def, negPart_min, neg_le_negPart, CFC.negPart_neg, continuous_negPart, negPart_nonpos', CFC.posPart_neg, negPart_nonneg, CFC.negPart_eq_of_eq_PosPart_sub, negPart_zero, posPart_inf_negPart_eq_zero, sub_abs_eq_neg_two_nsmul_negPart, MeromorphicOn.negPart_divisor_add_le_max, measurable_negPart, negPart_eq_zero, posPart_add_negPart, Function.locallyFinsuppWithin.nsmul_negPart, CStarAlgebra.norm_negPart_le, CFC.negPart_def, BoundedContinuousFunction.coe_negPart, MeromorphicOn.negPart_divisor_add_le_add, negPart_of_nonpos, negPart_eq_neg, negPart_eq_neg_inf_zero, negPart_pos, CStarAlgebra.nonneg_TFAE, posPart_negPart_injective, CFC.negPart_smul, posPart_neg, Function.locallyFinsuppWithin.restrict_negPart, Function.locallyFinsuppWithin.negPart_apply, CFC.negPart_smul_of_nonneg, abs_sub_eq_two_nsmul_negPart, CFC.posPart_negPart_unique, CFC.abs_sub_self, CFC.neg_negPart_le, negPart_neg, negPart_eq_ite_lt, negPart_add_posPart

OneLePart

Definitions

Name	Category	Theorems
oneLePart 📖	CompOp	35 math math: oneLePart_mono, oneLePart_eq_one, Pi.oneLePart_apply, oneLePart_leOnePart_injective, oneLePart_one, leOnePart_div_oneLePart, oneLePart_max, sup_eq_mul_oneLePart_div, oneLePart_min, oneLePart_eq_ite_lt, measurable_oneLePart, oneLePart_inv, oneLePart_of_one_le, le_oneLePart, inf_eq_div_oneLePart_div, oneLePart_inf_leOnePart_eq_one, one_lt_oneLePart, Measurable.oneLePart, leOnePart_inv, leOnePart_mul_oneLePart, oneLePart_le_one, mabs_mul_eq_oneLePart_sq, oneLePart_mul_leOnePart, one_lt_oneLePart_iff, oneLePart_def, le_iff_oneLePart_leOnePart, oneLePart_lt, oneLePart_of_le_one, oneLePart_leOnePart_inj, oneLePart_eq_self, Pi.oneLePart_def, oneLePart_eq_ite, oneLePart_div_leOnePart, mul_mabs_eq_oneLePart_sq, one_le_oneLePart

PosPart

Definitions

Name	Category	Theorems
posPart 📖	CompOp	76 math math: ValueDistribution.logCounting_zero, CFC.posPart_smul_of_nonpos, CFC.abs_add_self, CFC.posPart_one, posPart_max, CFC.posPart_natCast, inf_eq_sub_posPart_sub, posPart_eq_self, posPart_negPart_inj, CFC.negPart_mul_posPart, negPart_sub_posPart, add_abs_eq_two_nsmul_posPart, Function.locallyFinsuppWithin.nsmul_posPart, CFC.negPart_smul_of_nonpos, posPart_of_nonpos, le_iff_posPart_negPart, CFC.posPart_sub_negPart, BoundedContinuousFunction.coe_posPart, Function.locallyFinsuppWithin.posPart_add, posPart_nonneg, CFC.posPart_zero, CFC.posPart_eq_zero_iff, abs_add_eq_two_nsmul_posPart, CFC.posPart_mul_negPart, CFC.posPart_algebraMap_nnreal, posPart_zero, MeasureTheory.crossing_pos_eq, CFC.posPart_eq_zero_of_not_isSelfAdjoint, CStarAlgebra.norm_posPart_le, CFC.posPart_smul, MeasureTheory.Submartingale.pos, posPart_nonpos, CStarAlgebra.linear_combination_nonneg, posPart_def, posPart_pos_iff, posPart_eq_ite, posPart_sub_negPart, IsSelfAdjoint.norm_eq_max_norm_posPart_negPart, CFC.posPart_add_negPart, CFC.posPart_smul_of_nonneg, MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part, posPart_pos, CFC.negPart_neg, CFC.posPart_neg, Function.locallyFinsuppWithin.posPart_apply, Measurable.posPart, posPart_lt, Function.locallyFinsuppWithin.restrict_posPart, posPart_inf_negPart_eq_zero, posPart_add_negPart, Pi.posPart_def, CFC.posPart_algebraMap, Pi.posPart_apply, posPart_mono, CFC.posPart_nonneg, CFC.posPart_def, CFC.posPart_eq_self, le_posPart, CStarAlgebra.nonneg_TFAE, posPart_negPart_injective, continuous_posPart, posPart_neg, posPart_eq_zero, lipschitzWith_posPart, ValueDistribution.logCounting_coe, CFC.posPart_eq_of_eq_sub_negPart, CFC.posPart_negPart_unique, MeasureTheory.upcrossingsBefore_pos_eq, CFC.le_posPart, sup_eq_add_posPart_sub, negPart_neg, posPart_of_nonneg, posPart_min, measurable_posPart, posPart_eq_ite_lt, negPart_add_posPart

(root)

Definitions

Name	Category	Theorems
LeOnePart 📖	CompData	—
NegPart 📖	CompData	—
OneLePart 📖	CompData	—
«term_⁺» 📖	CompOp	—
«term_⁺ᵐ» 📖	CompOp	—
«term_⁻» 📖	CompOp	—
«term_⁻ᵐ» 📖	CompOp	—

---

← Back to Index