theorem Set.Finite.disjoint_of_sum_encard_le {α : Type u_1} {s t : Set α} (h : (s ∪ t).Finite) (hle : s.encard + t.encard ≤ (s ∪ t).encard) : Disjoint s t

theorem Set.Finite.encard_union_eq_add_encard_iff_disjoint {α : Type u_1} {s t : Set α} (h : (s ∪ t).Finite) : s.encard + t.encard = (s ∪ t).encard ↔ Disjoint s t

@[simp]

theorem encard_pair_le {α : Type u_1} (e f : α) : {e, f}.encard ≤ 2

theorem Set.Infinite.exists_finite_subset_encard_gt {α : Type u_1} {s : Set α} (hs : s.Infinite) (b : ℕ) : ∃ t ⊆ s, ↑b < t.encard ∧ t.Finite

theorem Set.coe_le_encard_iff {α : Type u_1} {s : Set α} {n : ℕ} : ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard

theorem Set.encard_le_cast_iff {α : Type u_1} {s : Set α} {n : ℕ} : s.encard ≤ ↑n ↔ ∃ (t : Finset α), ↑t = s ∧ t.card ≤ n

theorem Equiv.encard_univ_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) : _root_.Set.univ.encard = _root_.Set.univ.encard

theorem Equiv.encard_eq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) : s.encard = t.encard

theorem Fin.nonempty_embedding_iff_le_encard {α : Type u_1} {s : Set α} {n : ℕ} : Nonempty (Fin n ↪ ↑s) ↔ ↑n ≤ s.encard

@[simp]

theorem encard_univ_fin (a : ℕ) : Set.univ.encard = ↑a

theorem Fin.nonempty_equiv_iff_encard_eq {α : Type u_1} {s : Set α} {n : ℕ} : Nonempty (↑s ≃ Fin n) ↔ s.encard = ↑n

@[simp]

theorem ENat.card_option (α : Type u_3) : card (Option α) = card α + 1

theorem Set.encard_biUnion {α : Type u_1} {ι : Type u_3} {s : ι → Set α} {t : Finset ι} (ht : (↑t).PairwiseDisjoint s) : (⋃ i ∈ t, s i).encard = ∑ i ∈ t, (s i).encard

theorem Set.encard_iUnion {α : Type u_1} {ι : Type u_3} [Fintype ι] (s : ι → Set α) (hs : Pairwise (Function.onFun Disjoint s)) : (⋃ (i : ι), s i).encard = ∑ i : ι, (s i).encard

theorem Set.encard_biUnion_le {α : Type u_1} {ι : Type u_3} (I : Finset ι) (s : ι → Set α) : (⋃ i ∈ I, s i).encard ≤ ∑ i ∈ I, (s i).encard

theorem encard_iUnion_le {α : Type u_1} {ι : Type u_3} [Fintype ι] (s : ι → Set α) : (⋃ (i : ι), s i).encard ≤ ∑ i : ι, (s i).encard

theorem Finset.pairwiseDisjoint_of_sum_encard_le_encard_biUnion {α : Type u_1} {ι : Type u_3} {I : Finset ι} {s : ι → Set α} (hfin : ∀ i ∈ I, (s i).Finite) (hsum : ∑ i ∈ I, (s i).encard ≤ (⋃ i ∈ I, s i).encard) : (↑I).PairwiseDisjoint s

theorem pairwiseDisjoint_of_sum_encard_le_encard_iUnion {α : Type u_1} {ι : Type u_3} [Fintype ι] {s : ι → Set α} (hfin : ∀ (i : ι), (s i).Finite) (hsum : ∑ i : ι, (s i).encard ≤ (⋃ (i : ι), s i).encard) : Pairwise (Function.onFun Disjoint s)

theorem encard_biUnion_eq_sum_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} {u : Finset ι} {s : ι → Set α} (hs : ∀ i ∈ u, (s i).Finite) : (⋃ i ∈ u, s i).encard = ∑ i ∈ u, (s i).encard ↔ (↑u).PairwiseDisjoint s

theorem encard_iUnion_eq_sum_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [Fintype ι] {s : ι → Set α} (hfin : ∀ (i : ι), (s i).Finite) : (⋃ (i : ι), s i).encard = ∑ i : ι, (s i).encard ↔ Pairwise (Function.onFun Disjoint s)

theorem Set.Finite.encard_le_iff_nonempty_embedding {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) : s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)

theorem Set.Finite.encard_le_iff_nonempty_embedding' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (ht : t.Finite) : s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)

@[simp]

theorem finsum_mem_const {α : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Set α) (a : M) : ∑ᶠ (x : α) (_ : x ∈ s), a = s.ncard • a

theorem finsum_one {α : Type u_1} (s : Set α) : ∑ᶠ (x : α) (_ : x ∈ s), 1 = s.ncard