instance instAddEqTopClassENat : AddEqTopClass ℕ∞

instance instIsQuantaleENat_matroid : IsQuantale ℕ∞

theorem ENat.tsum_eq_top_of_support_infinite {α : Type u_2} {f : α → ℕ∞} (hf : (Function.support f).Infinite) : ∑' (a : α), f a = ⊤

theorem ENat.tsum_const_eq_top {ι : Type u_4} [Infinite ι] {c : ℕ∞} (hc : c ≠ 0) : ∑' (x : ι), c = ⊤

theorem ENat.tsum_eq_top_iff {α : Type u_2} {f : α → ℕ∞} : ∑' (a : α), f a = ⊤ ↔ (Function.support f).Infinite ∨ ∃ (a : α), f a = ⊤

theorem ENat.tsum_subtype_eq_top_iff {α : Type u_2} {f : α → ℕ∞} {s : Set α} : ∑' (a : ↑s), f ↑a = ⊤ ↔ (s ∩ Function.support f).Infinite ∨ ∃ a ∈ s, f a = ⊤

theorem ENat.tsum_subtype_eq_top_of_inter_support_infinite {α : Type u_2} {f : α → ℕ∞} {s : Set α} (hf : (s ∩ Function.support f).Infinite) : ∑' (a : ↑s), f ↑a = ⊤

theorem ENat.tsum_subtype_const_eq_top_of_ne_zero {α : Type u_2} {s : Set α} (hs : s.Infinite) {c : ℕ∞} (hc : c ≠ 0) : ∑' (x : ↑s), c = ⊤

@[simp]

theorem ENat.tsum_const {ι : Type u_1} (c : ℕ∞) : ∑' (x : ι), c = c * card ι

theorem ENat.tsum_one' {α : Type u_2} (s : Set α) : ∑' (i : ↑s), 1 ↑i = s.encard

A version of ENat.tsum_one where the 1 is explicitly a function from the type rather than from the subtype. Useful for rewriting.

@[simp]

theorem ENat.tsum_one {α : Type u_2} (s : Set α) : ∑' (x : ↑s), 1 = s.encard

@[simp]

theorem ENat.tsum_subtype_const {α : Type u_2} (s : Set α) (c : ℕ∞) : ∑' (x : ↑s), c = c * s.encard

theorem ENat.tsum_subtype_const' {α : Type u_2} (s : Set α) (c : ℕ∞) : ∑' (x : ↑s), (fun (x : α) => c) ↑x = c * s.encard

theorem ENat.encard_support_le_tsum {α : Type u_2} {f : α → ℕ∞} : (Function.support f).encard ≤ ∑' (x : α), f x

theorem ENat.tsum_ite_const {α : Type u_2} {P : α → Prop} {s t : ℕ∞} [DecidablePred P] : (∑' (x : α), if P x then s else t) = s * {x : α | P x}.encard + t * {x : α | ¬P x}.encard

theorem ENat.tsum_encard_eq_encard_iUnion {α : Type u_2} {ι : Type u_4} {s : ι → Set α} (hI : Pairwise (Function.onFun Disjoint s)) : ∑' (i : ι), (s i).encard = (⋃ (i : ι), s i).encard

theorem ENat.encard_iUnion_le_tsum_encard {α : Type u_2} {ι : Type u_4} {s : ι → Set α} : (⋃ (i : ι), s i).encard ≤ ∑' (i : ι), (s i).encard

theorem ENat.tsum_encard_eq_encard_biUnion {α : Type u_2} {ι : Type u_4} {s : ι → Set α} {t : Set ι} (hI : t.PairwiseDisjoint s) : ∑' (i : ↑t), (s ↑i).encard = (⋃ i ∈ t, s i).encard

theorem ENat.encard_biUnion_le_tsum_encard {α : Type u_2} {ι : Type u_4} {s : ι → Set α} {I : Set ι} : (⋃ i ∈ I, s i).encard ≤ ∑' (i : ↑I), (s ↑i).encard

theorem ENat.encard_eq_tsum_ite {α : Type u_2} (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : s.encard = ∑' (x : α), if x ∈ s then 1 else 0

theorem ENat.tsum_encard_eq_encard_biUnion_iff {α : Type u_2} {ι : Type u_4} {s : ι → Set α} {t : Set ι} (hfin : (⋃ i ∈ t, s i).Finite) : ∑' (i : ↑t), (s ↑i).encard = (⋃ i ∈ t, s i).encard ↔ t.PairwiseDisjoint s

theorem ENat.tsum_encard_eq_encard_iUnion_iff {α : Type u_2} {ι : Type u_4} {s : ι → Set α} (hfin : (⋃ (i : ι), s i).Finite) : ∑' (i : ι), (s i).encard = (⋃ (i : ι), s i).encard ↔ Pairwise (Function.onFun Disjoint s)

theorem ENat.tsum_encard_eq_encard_sUnion {α : Type u_2} {c : Set (Set α)} (hc : c.PairwiseDisjoint id) : ∑' (t : ↑c), (↑t).encard = (⋃₀ c).encard

theorem ENat.encard_sUnion_le_tsum_encard {α : Type u_2} {c : Set (Set α)} : (⋃₀ c).encard ≤ ∑' (s : ↑c), (↑s).encard

theorem ENat.tsum_inter_fiber_eq {α : Type u_2} {ι : Type u_4} {s : Set ι} (f : ι → α) : ∑' (a : α), (s ∩ f ⁻¹' {a}).encard = s.encard

theorem ENat.tsum_fiber_eq {α : Type u_2} {ι : Type u_4} (f : ι → α) : ∑' (a : α), (f ⁻¹' {a}).encard = Set.univ.encard