Cardinalities of images, complements, coverings, division preimages, sigma fibres and doubled sets

Two maps on a common index type that identify the same pairs of indices take equally many values on every set of indices (Set.encard_image_eq_encard_image_of_eq_iff): the second map factors through the first by a map that is injective on its values.

For n > 0, every natural number j is the quotient i / n of exactly the n natural numbers n * j, …, n * j + n - 1. Hence for n > 0 the preimage of a finite set S ⊆ ℕ under i ↦ i / n has n times as many elements as S. This is the counting fact behind sequences that repeat each term n times, such as the singular values of a block sum of n copies of one map.

Adding a fresh element to a set removes one element from its complement (Set.encard_compl_insert_add_one).

The points of the range of an injective map φ into a sigma type that lie in the fibre over i are counted by the arguments that φ maps into that fibre (Set.ncard_preimage_sigmaMk_range).

A property read off the same function on both copies of ι in ι ⊕ ι holds on twice as many indices as on ι (Set.ncard_setOf_sumElim).

For an injective map f from a finite type into a linear order, the number of indices whose value lies below f a determines a (Set.injective_ncard_setOf_lt): it is the rank of f a among the values of f. Each j < Nat.card ι is the rank of exactly one index (Set.encard_setOf_ncard_setOf_lt_eq).

A set covered by finitely many finite sets C i is finite, with at most ∑ i, |C i| elements (Set.finite_and_ncard_le_sum_of_subset_biUnion).

A set of naturals with at most n elements up to 2n, for every n, leaves at least n + 1 numbers up to 2n outside it, so its complement is infinite (Set.infinite_compl_of_ncard_inter_Iic_le). Constructions of simple sets obtain coinfiniteness from this counting invariant.

The statement Set.ncard_preimage_div needs no hypotheses: Set.ncard is 0 on infinite sets, and i / 0 = 0 makes the preimage under division by zero either ∅ or all of ℕ, so both sides are 0 when S is infinite or n = 0.

theorem Set.encard_image_eq_encard_image_of_eq_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ι → α} {g : ι → β} (h : ∀ (i j : ι), f i = f j ↔ g i = g j) (I : Set ι) : (f '' I).encard = (g '' I).encard

Two maps that identify the same pairs of indices take equally many values on every set of indices.

theorem Set.encard_compl_insert_add_one {α : Type u_1} {s : Set α} {x : α} (hx : x ∉ s) : (insert x s)ᶜ.encard + 1 = sᶜ.encard

Adding a fresh element to a set removes one element from its complement.

theorem Set.ncard_preimage_sigmaMk_range {κ : Type u_1} {α : Type u_2} {Y : κ → Type u_3} {φ : α → (i : κ) × Y i} (hφ : Function.Injective φ) (i : κ) : (Sigma.mk i ⁻¹' range φ).ncard = {a : α | (φ a).fst = i}.ncard

The points of the range of an injective map into a sigma type lying over the index i are counted by the arguments mapped over i.

theorem Set.finite_and_ncard_le_sum_of_subset_biUnion {ι : Type u_1} {α : Type u_2} {S : Set α} {t : Finset ι} {C : ι → Set α} {b : ι → ℕ} (hS : S ⊆ ⋃ i ∈ t, C i) (hC : ∀ i ∈ t, (C i).Finite ∧ (C i).ncard ≤ b i) : S.Finite ∧ S.ncard ≤ ∑ i ∈ t, b i

A set covered by the sets C i, i ∈ t, each finite with at most b i elements, is finite with at most ∑ i ∈ t, b i elements. The sets C i may overlap.

theorem Set.infinite_compl_of_ncard_inter_Iic_le {A : Set ℕ} (hA : ∀ (n : ℕ), (A ∩ Iic (2 * n)).ncard ≤ n) : Aᶜ.Infinite

The counting invariant gives coinfiniteness. A set of naturals with at most n elements up to 2 * n, for every n, has an infinite complement.

theorem Set.ncard_preimage_div (S : Set ℕ) (n : ℕ) : ((fun (x : ℕ) => x / n) ⁻¹' S).ncard = S.ncard * n

The preimage of a set S ⊆ ℕ under i ↦ i / n has n times as many elements as S. Both sides are 0 when S is infinite or n = 0.

theorem Set.injective_ncard_setOf_lt {ι : Type u_1} {α : Type u_2} [Finite ι] [LinearOrder α] {f : ι → α} (hf : Function.Injective f) : Function.Injective fun (a : ι) => {i : ι | f i < f a}.ncard

For an injective map f from a finite type into a linear order, the number of indices whose value lies below f a determines a.

theorem Set.encard_setOf_ncard_setOf_lt_eq {ι : Type u_1} {α : Type u_2} [Finite ι] [LinearOrder α] {f : ι → α} (hf : Function.Injective f) (j : ℕ) : {k : ι | {i : ι | f i < f k}.ncard = j}.encard = if j < Nat.card ι then 1 else 0

For an injective map f from a finite type into a linear order, every j < Nat.card ι is the number of indices whose value lies below f k for exactly one index k, and no larger j is.

theorem Set.ncard_setOf_sumElim {ι : Type u_1} {β : Type u_2} (f : ι → β) (P : β → Prop) : {j : ι ⊕ ι | P (Sum.elim f f j)}.ncard = 2 * {i : ι | P (f i)}.ncard

A property of the doubled index set ι ⊕ ι, read off the same function on both copies of ι, holds on twice as many indices as on ι. Both sides are 0 when the set on ι is infinite.