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

@[simp]

theorem encard_pair_iff {α : Type u_1} (e f : α) : {e, f}.encard = 2 ↔ e ≠ f

theorem two_le_encard_iff_nontrivial {α : Type u_1} {s : Set α} : 2 ≤ s.encard ↔ s.Nontrivial

theorem Nonempty.one_le_encard {α : Type u_1} {s : Set α} (hs : s.Nonempty) : 1 ≤ s.encard

theorem Nontrivial.two_le_encard {α : Type u_1} {s : Set α} (hs : s.Nontrivial) : 2 ≤ s.encard

theorem Subsingleton.encard_le_one {α : Type u_1} {s : Set α} (hs : s.Subsingleton) : s.encard ≤ 1

theorem encard_le_encard_diff_singleton_add_one {α : Type u_1} (s : Set α) (x : α) : s.encard ≤ (s \ {x}).encard + 1

theorem encard_add_one_le_of_ssubset {α : Type u_1} {s t : Set α} (hst : s ⊂ t) : s.encard + 1 ≤ t.encard

theorem succ_le_encard_iff {α : Type u_1} {s : Set α} {n : ℕ∞} : n + 1 ≤ s.encard ↔ ∃ x ∈ s, n ≤ (s \ {x}).encard

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.Infinite.exists_finite_subset_encard_gt' {α : Type u_1} {s : Set α} (hs : s.Infinite) {b : ℕ∞} (hb : b ≠ ⊤) : ∃ t ⊆ s, b < t.encard ∧ t.Finite

a version of Set.Infinite.exists_finite_subset_encard_gt with b of type ℕ∞

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 finite_of_encard_eq_ofNat {α : Type u_1} {s : Set α} {n : ℕ} [n.AtLeastTwo] (h : s.encard = OfNat.ofNat n) : s.Finite

theorem finite_of_encard_le_ofNat {α : Type u_1} {s : Set α} {n : ℕ} [n.AtLeastTwo] (h : s.encard ≤ OfNat.ofNat n) : s.Finite

theorem finite_of_encard_eq_one {α : Type u_1} {s : Set α} (h : s.encard = 1) : s.Finite

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

theorem ENat.card_coe_setOf_ne {α : Type u_1} (a : α) : card ↑{i : α | i ≠ a} = card α - 1

theorem List.encard_toSet_le {α : Type u_1} (L : List α) : {x : α | x ∈ L}.encard ≤ ↑L.length

theorem List.Nodup.encard_toSet_eq {α : Type u_1} {L : List α} (hL : L.Nodup) : {x : α | x ∈ L}.encard = ↑L.length

theorem Set.eq_of_encard_le_two_of_mem_of_mem {α : Type u_1} {s : Set α} {x y : α} (hs : s.encard ≤ 2) (hxs : x ∈ s) (hys : y ∈ s) (hxy : x ≠ y) : s = {x, y}

theorem Set.exists_eq_of_encard_eq_two_of_mem {α : Type u_1} {s : Set α} {x : α} (hs : s.encard = 2) (hxs : x ∈ s) : ∃ (y : α), y ≠ x ∧ s = {x, y}

theorem Set.exists_eq_of_encard_eq_three_of_mem {α : Type u_1} {s : Set α} {x : α} (hs : s.encard = 3) (hxs : x ∈ s) : ∃ (y : α) (z : α), y ≠ x ∧ z ≠ x ∧ y ≠ z ∧ s = {x, y, z}

theorem Set.exists_eq_of_encard_eq_three_of_mem_of_mem {α : Type u_1} {s : Set α} {x y : α} (hs : s.encard = 3) (hxs : x ∈ s) (hys : y ∈ s) (hxy : x ≠ y) : ∃ (z : α), z ≠ x ∧ z ≠ y ∧ s = {x, y, z}

theorem Set.eq_of_encard_le_three_of_mem_of_mem_of_mem {α : Type u_1} {s : Set α} {x y z : α} (hs : s.encard ≤ 3) (hxs : x ∈ s) (hys : y ∈ s) (hzs : z ∈ s) (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) : s = {x, y, z}

theorem nonempty_of_ofNat_le_encard {α : Type u_1} {s : Set α} {n : ℕ} [n.AtLeastTwo] (hs : OfNat.ofNat n ≤ s.encard) : s.Nonempty

theorem exists_of_encard_add_encard_eq_one {α : Type u_1} {s t : Set α} (h : s.encard + t.encard = 1) : ∃ (x : α), s = ∅ ∧ t = {x} ∨ s = {x} ∧ t = ∅

theorem exists_of_encard_add_encard_eq_two {α : Type u_1} {s t : Set α} (h : s.encard + t.encard = 2) (hdj : Disjoint s t) : ∃ (x : α) (y : α), x ≠ y ∧ (s = ∅ ∧ t = {x, y} ∨ s = {x} ∧ t = {y} ∨ s = {x, y} ∧ t = ∅)

theorem exists_of_encard_add_encard_eq_three {α : Type u_1} {s t : Set α} (h : s.encard + t.encard = 3) (hdj : Disjoint s t) : ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ (s = ∅ ∧ t = {x, y, z} ∨ s = {x} ∧ t = {y, z} ∨ s = {x, y} ∧ t = {z} ∨ s = {x, y, z} ∧ t = ∅)

@[simp]

theorem ENat.encard_Iio (n : ℕ∞) : (Set.Iio n).encard = n

@[simp]

theorem ENat.encard_Iic (n : ℕ∞) : (Set.Iic n).encard = n + 1