IndicatorCard

📁 Source: Mathlib/Algebra/Order/Archimedean/IndicatorCard.lean

Statistics

Metric	Count
Definitions	0
Theorems infinite_iff_tendsto_sum_indicator_atTop, limsup_eq_tendsto_sum_indicator_atTop, sum_indicator_eventually_eq_card	3
Total	3

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinite_iff_tendsto_sum_indicator_atTop 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Infinite Filter.Tendsto Finset.sum Finset.range indicator Filter.atTop Nat.instPreorder	—	Monotone.comp Finset.sum_mono_set_of_nonneg IsOrderedAddMonoid.toAddLeftMono indicator_nonneg LT.lt.le Finset.range_mono Monotone.tendsto_atTop_atTop_iff instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat exists_lt_nsmul Infinite.exists_subset_card_eq Finset.bddAbove le_imp_le_of_le_of_le le_of_lt le_refl Finset.sum_le_sum indicator_le_indicator_apply_of_subset Finset.mem_range LE.le.trans_lt lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instIsOrderedAddMonoid Finset.sum_indicator_subset Finset.sum_eq_card_nsmul Mathlib.Tactic.Contrapose.contrapose₁ Filter.tendsto_congr' sum_indicator_eventually_eq_card Filter.tendsto_atTop_atTop Mathlib.Tactic.Push.not_forall_eq not_le_of_gt
limsup_eq_tendsto_sum_indicator_atTop 📖	mathematical	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Filter.limsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra Filter.atTop Nat.instPreorder setOf Filter.Tendsto Finset.sum Finset.range indicator	—	Nat.cofinite_eq_atTop Filter.cofinite.limsup_set_eq ext mem_setOf_eq infinite_iff_tendsto_sum_indicator_atTop iff_eq_eq
sum_indicator_eventually_eq_card 📖	mathematical	—	Filter.Eventually Finset.sum Finset.range indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoid.toNatSMul Nat.card Elem Filter.atTop Nat.instPreorder	—	indicator_of_mem Finite.mem_toFinset Nat.card_eq_card_finite_toFinset Finset.sum_eq_card_nsmul Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Finite.bddAbove Finset.sum_subset Finset.mem_range LE.le.trans_lt mem_upperBounds indicator_of_notMem

---

← Back to Index