Indicator

📁 Source: Mathlib/Analysis/Normed/Group/Indicator.lean

Statistics

Metric	Count
Definitions	0
Theorems enorm_indicator_eq_indicator_enorm, enorm_indicator_le_enorm_self, enorm_indicator_le_of_subset, indicator_enorm_le_enorm_self, indicator_norm_le_norm_self, nnnorm_indicator_eq_indicator_nnnorm, norm_indicator_eq_indicator_norm, norm_indicator_le_norm_self, norm_indicator_le_of_subset	9
Total	9

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enorm_indicator_eq_indicator_enorm 📖	mathematical	—	ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ENNReal instZeroENNReal	—	Set.indicator_comp_of_zero enorm_zero
enorm_indicator_le_enorm_self 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid	—	enorm_indicator_eq_indicator_enorm indicator_enorm_le_enorm_self
enorm_indicator_le_of_subset 📖	mathematical	Set Set.instHasSubset	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid	—	enorm_indicator_eq_indicator_enorm le_imp_le_of_le_of_le Set.indicator_le_indicator_apply_of_subset zero_le ENNReal.instCanonicallyOrderedAdd le_refl
indicator_enorm_le_enorm_self 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Set.indicator instZeroENNReal ENorm.enorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm	—	Set.indicator_le_self' zero_le ENNReal.instCanonicallyOrderedAdd
indicator_norm_le_norm_self 📖	mathematical	—	Real Real.instLE Set.indicator Real.instZero Norm.norm SeminormedAddGroup.toNorm	—	Set.indicator_le_self' norm_nonneg
nnnorm_indicator_eq_indicator_nnnorm 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup NNReal instZeroNNReal	—	Set.indicator_comp_of_zero nnnorm_zero
norm_indicator_eq_indicator_norm 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Real Real.instZero	—	Set.indicator_comp_of_zero norm_zero
norm_indicator_le_norm_self 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup	—	norm_indicator_eq_indicator_norm indicator_norm_le_norm_self
norm_indicator_le_of_subset 📖	mathematical	Set Set.instHasSubset	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup	—	norm_indicator_eq_indicator_norm le_imp_le_of_le_of_le Set.indicator_le_indicator_apply_of_subset norm_nonneg le_refl

---

← Back to Index