Mathlib.SetTheory.Cardinal.Arithmetic

Cardinal.mul_eq_self theorem

{c : Cardinal} (h : ℵ₀ ≤ c) : c * c = c

Full source

/-- If `α` is an infinite type, then `α × α` and `α` have the same cardinality. -/
theorem mul_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c * c = c := by
  refine le_antisymm ?_ (by simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans h) c)
  -- the only nontrivial part is `c * c ≤ c`. We prove it inductively.
  refine Acc.recOn (Cardinal.lt_wf.apply c) (fun c _ => Cardinal.inductionOn c fun α IH ol => ?_) h
  -- consider the minimal well-order `r` on `α` (a type with cardinality `c`).
  rcases ord_eq α with ⟨r, wo, e⟩
  classical
  letI := linearOrderOfSTO r
  haveI : IsWellOrder α (· < ·) := wo
  -- Define an order `s` on `α × α` by writing `(a, b) < (c, d)` if `max a b < max c d`, or
  -- the max are equal and `a < c`, or the max are equal and `a = c` and `b < d`.
  let g : α × α → α := fun p => max p.1 p.2
  let f : α × αα × α ↪ Ordinal × α × α :=
    ⟨fun p : α × α => (typein (· < ·) (g p), p), fun p q => congr_arg Prod.snd⟩
  let s := f ⁻¹'o Prod.Lex (· < ·) (Prod.Lex (· < ·) (· < ·))
  -- this is a well order on `α × α`.
  haveI : IsWellOrder _ s := (RelEmbedding.preimage _ _).isWellOrder
  /- it suffices to show that this well order is smaller than `r`
       if it were larger, then `r` would be a strict prefix of `s`. It would be contained in
      `β × β` for some `β` of cardinality `< c`. By the inductive assumption, this set has the
      same cardinality as `β` (or it is finite if `β` is finite), so it is `< c`, which is a
      contradiction. -/
  suffices type s ≤ type r by exact card_le_card this
  refine le_of_forall_lt fun o h => ?_
  rcases typein_surj s h with ⟨p, rfl⟩
  rw [← e, lt_ord]
  refine lt_of_le_of_lt
    (?_ : _ ≤ card (succ (typein (· < ·) (g p))) * card (succ (typein (· < ·) (g p)))) ?_
  · have : { q | s q p }{ q | s q p } ⊆ insert (g p) { x | x < g p } ×ˢ insert (g p) { x | x < g p } := by
      intro q h
      simp only [s, f, Preimage, Embedding.coeFn_mk, Prod.lex_def, typein_lt_typein,
        typein_inj, mem_setOf_eq] at h
      exact max_le_iff.1 (le_iff_lt_or_eq.2 <| h.imp_right And.left)
    suffices H : (insert (g p) { x | r x (g p) } : Set α) ≃ { x | r x (g p) } ⊕ PUnit from
      ⟨(Set.embeddingOfSubset _ _ this).trans
        ((Equiv.Set.prod _ _).trans (H.prodCongr H)).toEmbedding⟩
    refine (Equiv.Set.insert ?_).trans ((Equiv.refl _).sumCongr punitEquivPUnit)
    apply @irrefl _ r
  rcases lt_or_le (card (succ (typein (· < ·) (g p)))) ℵ₀ with qo | qo
  · exact (mul_lt_aleph0 qo qo).trans_le ol
  · suffices (succ (typein LT.lt (g p))).card < #α from (IH _ this qo).trans_lt this
    rw [← lt_ord]
    apply (isLimit_ord ol).succ_lt
    rw [e]
    apply typein_lt_type

Infinite Cardinal Multiplication Identity: $c \times c = c$ for $\aleph_0 \leq c$

Informal description

For any infinite cardinal number $c$ (i.e., $\aleph_0 \leq c$), the product $c \times c$ is equal to $c$.

Cardinal.mul_eq_max theorem

{a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : ℵ₀ ≤ b) : a * b = max a b

Full source

/-- If `α` and `β` are infinite types, then the cardinality of `α × β` is the maximum
of the cardinalities of `α` and `β`. -/
theorem mul_eq_max {a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : ℵ₀ ≤ b) : a * b = max a b :=
  le_antisymm
      (mul_eq_self (ha.trans (le_max_left a b)) ▸
        mul_le_mul' (le_max_left _ _) (le_max_right _ _)) <|
    max_le (by simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans hb) a)
      (by simpa only [one_mul] using mul_le_mul_right' (one_le_aleph0.trans ha) b)

Product of Infinite Cardinals Equals Their Maximum

Informal description

For any two infinite cardinal numbers $a$ and $b$ (i.e., $\aleph_0 \leq a$ and $\aleph_0 \leq b$), the product $a \times b$ is equal to the maximum of $a$ and $b$, i.e., $a \times b = \max(a, b)$.

Cardinal.mul_mk_eq_max theorem

{α β : Type u} [Infinite α] [Infinite β] : #α * #β = max #α #β

Full source

@[simp]
theorem mul_mk_eq_max {α β : Type u} [Infinite α] [Infinite β] : #α * #β = max #α #β :=
  mul_eq_max (aleph0_le_mk α) (aleph0_le_mk β)

Product of Cardinalities of Infinite Types Equals Their Maximum

Informal description

For any infinite types $\alpha$ and $\beta$, the product of their cardinalities equals the maximum of their cardinalities, i.e., $\#\alpha \times \#\beta = \max(\#\alpha, \#\beta)$.

Cardinal.aleph_mul_aleph theorem

(o₁ o₂ : Ordinal) : ℵ_ o₁ * ℵ_ o₂ = ℵ_ (max o₁ o₂)

Full source

@[simp]
theorem aleph_mul_aleph (o₁ o₂ : Ordinal) : ℵ_ o₁ * ℵ_ o₂ = ℵ_ (max o₁ o₂) := by
  rw [Cardinal.mul_eq_max (aleph0_le_aleph o₁) (aleph0_le_aleph o₂), aleph_max]

Product of Aleph Numbers Equals Aleph of Maximum Ordinals

Informal description

For any two ordinal numbers $o₁$ and $o₂$, the product of the corresponding aleph numbers satisfies $\aleph_{o₁} \times \aleph_{o₂} = \aleph_{\max(o₁, o₂)}$.

Cardinal.aleph0_mul_eq theorem

{a : Cardinal} (ha : ℵ₀ ≤ a) : ℵ₀ * a = a

Full source

@[simp]
theorem aleph0_mul_eq {a : Cardinal} (ha : ℵ₀ ≤ a) : ℵ₀ * a = a :=
  (mul_eq_max le_rfl ha).trans (max_eq_right ha)

Product of Aleph-null with Infinite Cardinal: $\aleph_0 \times a = a$

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$), the product of $\aleph_0$ and $a$ equals $a$, i.e., $\aleph_0 \times a = a$.

Cardinal.mul_aleph0_eq theorem

{a : Cardinal} (ha : ℵ₀ ≤ a) : a * ℵ₀ = a

Full source

@[simp]
theorem mul_aleph0_eq {a : Cardinal} (ha : ℵ₀ ≤ a) : a * ℵ₀ = a :=
  (mul_eq_max ha le_rfl).trans (max_eq_left ha)

Product with Aleph-null Equals Original Cardinal for Infinite Cardinals

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$), the product of $a$ with $\aleph_0$ is equal to $a$, i.e., $a \times \aleph_0 = a$.

Cardinal.aleph0_mul_mk_eq theorem

{α : Type*} [Infinite α] : ℵ₀ * #α = #α

Full source

theorem aleph0_mul_mk_eq {α : Type*} [Infinite α] : ℵ₀ * #α = #α :=
  aleph0_mul_eq (aleph0_le_mk α)

Product of Aleph-null with Cardinality of Infinite Type Equals Its Cardinality: $\aleph_0 \times \#\alpha = \#\alpha$

Informal description

For any infinite type $\alpha$, the product of the cardinal number $\aleph_0$ and the cardinality of $\alpha$ equals the cardinality of $\alpha$, i.e., $\aleph_0 \times \#\alpha = \#\alpha$.

Cardinal.mk_mul_aleph0_eq theorem

{α : Type*} [Infinite α] : #α * ℵ₀ = #α

Full source

theorem mk_mul_aleph0_eq {α : Type*} [Infinite α] : #α * ℵ₀ = #α :=
  mul_aleph0_eq (aleph0_le_mk α)

Cardinal Multiplication Identity: $\#\alpha \times \aleph_0 = \#\alpha$ for Infinite $\alpha$

Informal description

For any infinite type $\alpha$, the cardinality of $\alpha$ multiplied by $\aleph_0$ equals the cardinality of $\alpha$, i.e., $\#\alpha \times \aleph_0 = \#\alpha$.

Cardinal.aleph0_mul_aleph theorem

(o : Ordinal) : ℵ₀ * ℵ_ o = ℵ_ o

Full source

@[simp]
theorem aleph0_mul_aleph (o : Ordinal) : ℵ₀ * ℵ_ o = ℵ_ o :=
  aleph0_mul_eq (aleph0_le_aleph o)

Product of Aleph-null with Aleph Number: $\aleph_0 \times \aleph_o = \aleph_o$

Informal description

For any ordinal number $o$, the product of the first infinite cardinal $\aleph_0$ with the aleph number $\aleph_o$ equals $\aleph_o$, i.e., $\aleph_0 \times \aleph_o = \aleph_o$.

Cardinal.aleph_mul_aleph0 theorem

(o : Ordinal) : ℵ_ o * ℵ₀ = ℵ_ o

Full source

@[simp]
theorem aleph_mul_aleph0 (o : Ordinal) : ℵ_ o * ℵ₀ = ℵ_ o :=
  mul_aleph0_eq (aleph0_le_aleph o)

Product of Aleph Number with Aleph-null: $\aleph_o \times \aleph_0 = \aleph_o$

Informal description

For any ordinal number $o$, the product of the aleph number $\aleph_o$ with $\aleph_0$ equals $\aleph_o$, i.e., $\aleph_o \times \aleph_0 = \aleph_o$.

Cardinal.mul_lt_of_lt theorem

{a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b < c) : a * b < c

Full source

theorem mul_lt_of_lt {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b < c) : a * b < c :=
  (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt <|
    (lt_or_le (max a b) ℵ₀).elim (fun h => (mul_lt_aleph0 h h).trans_le hc) fun h => by
      rw [mul_eq_self h]
      exact max_lt h1 h2

Product of Cardinals Below an Infinite Cardinal is Below It

Informal description

For any infinite cardinal number $c$ (i.e., $\aleph_0 \leq c$) and any cardinals $a, b$ such that $a < c$ and $b < c$, the product $a \times b$ is strictly less than $c$.

Cardinal.mul_le_max_of_aleph0_le_left theorem

{a b : Cardinal} (h : ℵ₀ ≤ a) : a * b ≤ max a b

Full source

theorem mul_le_max_of_aleph0_le_left {a b : Cardinal} (h : ℵ₀ ≤ a) : a * b ≤ max a b := by
  convert mul_le_mul' (le_max_left a b) (le_max_right a b) using 1
  rw [mul_eq_self]
  exact h.trans (le_max_left a b)

Product of Infinite Cardinals is Bounded by Maximum ($\aleph_0 \leq a$)

Informal description

For any infinite cardinal numbers $a$ and $b$ such that $\aleph_0 \leq a$, the product $a \times b$ is less than or equal to the maximum of $a$ and $b$, i.e., $a \times b \leq \max(a, b)$.

Cardinal.mul_eq_max_of_aleph0_le_left theorem

{a b : Cardinal} (h : ℵ₀ ≤ a) (h' : b ≠ 0) : a * b = max a b

Full source

theorem mul_eq_max_of_aleph0_le_left {a b : Cardinal} (h : ℵ₀ ≤ a) (h' : b ≠ 0) :
    a * b = max a b := by
  rcases le_or_lt ℵ₀ b with hb | hb
  · exact mul_eq_max h hb
  refine (mul_le_max_of_aleph0_le_left h).antisymm ?_
  have : b ≤ a := hb.le.trans h
  rw [max_eq_left this]
  convert mul_le_mul_left' (one_le_iff_ne_zero.mpr h') a
  rw [mul_one]

Product of Infinite and Nonzero Cardinals Equals Their Maximum ($\aleph_0 \leq a$)

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$) and any nonzero cardinal $b$, the product $a \times b$ equals the maximum of $a$ and $b$, i.e., $a \times b = \max(a, b)$.

Cardinal.mul_le_max_of_aleph0_le_right theorem

{a b : Cardinal} (h : ℵ₀ ≤ b) : a * b ≤ max a b

Full source

theorem mul_le_max_of_aleph0_le_right {a b : Cardinal} (h : ℵ₀ ≤ b) : a * b ≤ max a b := by
  simpa only [mul_comm b, max_comm b] using mul_le_max_of_aleph0_le_left h

Product of Infinite Cardinals is Bounded by Maximum ($\aleph_0 \leq b$)

Informal description

For any infinite cardinal numbers $a$ and $b$ such that $\aleph_0 \leq b$, the product $a \times b$ is less than or equal to the maximum of $a$ and $b$, i.e., $a \times b \leq \max(a, b)$.

Cardinal.mul_eq_max_of_aleph0_le_right theorem

{a b : Cardinal} (h' : a ≠ 0) (h : ℵ₀ ≤ b) : a * b = max a b

Full source

theorem mul_eq_max_of_aleph0_le_right {a b : Cardinal} (h' : a ≠ 0) (h : ℵ₀ ≤ b) :
    a * b = max a b := by
  rw [mul_comm, max_comm]
  exact mul_eq_max_of_aleph0_le_left h h'

Product of Nonzero and Infinite Cardinals Equals Their Maximum ($\aleph_0 \leq b$)

Informal description

For any nonzero cardinal number $a$ and any infinite cardinal number $b$ (i.e., $\aleph_0 \leq b$), the product $a \times b$ equals the maximum of $a$ and $b$, i.e., $a \times b = \max(a, b)$.

Cardinal.mul_eq_max' theorem

{a b : Cardinal} (h : ℵ₀ ≤ a * b) : a * b = max a b

Full source

theorem mul_eq_max' {a b : Cardinal} (h : ℵ₀ ≤ a * b) : a * b = max a b := by
  rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩
  · exact mul_eq_max_of_aleph0_le_left ha' hb
  · exact mul_eq_max_of_aleph0_le_right ha hb'

Product of Cardinals Equals Maximum When Infinite ($\aleph_0 \leq a \cdot b$)

Informal description

For any two cardinal numbers $a$ and $b$, if the product $a \cdot b$ is infinite (i.e., $\aleph_0 \leq a \cdot b$), then $a \cdot b = \max(a, b)$.

Cardinal.mul_le_max theorem

(a b : Cardinal) : a * b ≤ max (max a b) ℵ₀

Full source

theorem mul_le_max (a b : Cardinal) : a * b ≤ max (max a b) ℵ₀ := by
  rcases eq_or_ne a 0 with (rfl | ha0); · simp
  rcases eq_or_ne b 0 with (rfl | hb0); · simp
  rcases le_or_lt ℵ₀ a with ha | ha
  · rw [mul_eq_max_of_aleph0_le_left ha hb0]
    exact le_max_left _ _
  · rcases le_or_lt ℵ₀ b with hb | hb
    · rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

Product of Cardinals Bounded by Maximum and Aleph-null

Informal description

For any two cardinal numbers $a$ and $b$, their product $a \times b$ is less than or equal to the maximum of $\max(a, b)$ and $\aleph_0$, i.e., $a \times b \leq \max(\max(a, b), \aleph_0)$.

Cardinal.mul_eq_left theorem

{a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : b ≤ a) (hb' : b ≠ 0) : a * b = a

Full source

theorem mul_eq_left {a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : b ≤ a) (hb' : b ≠ 0) : a * b = a := by
  rw [mul_eq_max_of_aleph0_le_left ha hb', max_eq_left hb]

Product of Infinite Cardinal with Smaller Nonzero Cardinal Equals Itself

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$) and any nonzero cardinal $b$ with $b \leq a$, the product $a \times b$ equals $a$.

Cardinal.mul_eq_right theorem

{a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a ≤ b) (ha' : a ≠ 0) : a * b = b

Full source

theorem mul_eq_right {a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a ≤ b) (ha' : a ≠ 0) : a * b = b := by
  rw [mul_comm, mul_eq_left hb ha ha']

Product of Nonzero Cardinal with Infinite Cardinal Equals the Infinite Cardinal

Informal description

For any infinite cardinal number $b$ (i.e., $\aleph_0 \leq b$) and any nonzero cardinal $a$ with $a \leq b$, the product $a \times b$ equals $b$.

Cardinal.le_mul_left theorem

{a b : Cardinal} (h : b ≠ 0) : a ≤ b * a

Full source

theorem le_mul_left {a b : Cardinal} (h : b ≠ 0) : a ≤ b * a := by
  convert mul_le_mul_right' (one_le_iff_ne_zero.mpr h) a
  rw [one_mul]

Left Multiplication Preserves Cardinal Order: $a \leq b \cdot a$ for $b \neq 0$

Informal description

For any cardinal numbers $a$ and $b$ with $b \neq 0$, we have $a \leq b \cdot a$.

Cardinal.le_mul_right theorem

{a b : Cardinal} (h : b ≠ 0) : a ≤ a * b

Full source

theorem le_mul_right {a b : Cardinal} (h : b ≠ 0) : a ≤ a * b := by
  rw [mul_comm]
  exact le_mul_left h

Right Multiplication Preserves Cardinal Order: $a \leq a \cdot b$ for $b \neq 0$

Informal description

For any cardinal numbers $a$ and $b$ with $b \neq 0$, we have $a \leq a \cdot b$.

Cardinal.mul_eq_left_iff theorem

{a b : Cardinal} : a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Full source

theorem mul_eq_left_iff {a b : Cardinal} : a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 := by
  rw [max_le_iff]
  refine ⟨fun h => ?_, ?_⟩
  · rcases le_or_lt ℵ₀ a with ha | ha
    · have : a ≠ 0 := by
        rintro rfl
        exact ha.not_lt aleph0_pos
      left
      rw [and_assoc]
      use ha
      constructor
      · rw [← not_lt]
        exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
      · rintro rfl
        apply this
        rw [mul_zero] at h
        exact h.symm
    right
    by_cases h2a : a = 0
    · exact Or.inr h2a
    have hb : b ≠ 0 := by
      rintro rfl
      apply h2a
      rw [mul_zero] at h
      exact h.symm
    left
    rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
    · contradiction
    · contradiction
    rw [← Ne] at h2a
    rw [← one_le_iff_ne_zero] at h2a hb
    norm_cast at h2a hb h ⊢
    apply le_antisymm _ hb
    rw [← not_lt]
    apply fun h2b => ne_of_gt _ h
    conv_rhs => left; rw [← mul_one n]
    rw [Nat.mul_lt_mul_left]
    · exact id
    apply Nat.lt_of_succ_le h2a
  · rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)
    · rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
    all_goals simp

Characterization of when $a \times b = a$ for cardinals

Informal description

For any cardinal numbers $a$ and $b$, the equality $a \times b = a$ holds if and only if one of the following conditions is satisfied: 1. Both $\max(\aleph_0, b) \leq a$ and $b \neq 0$, or 2. $b = 1$, or 3. $a = 0$.

Cardinal.add_eq_self theorem

{c : Cardinal} (h : ℵ₀ ≤ c) : c + c = c

Full source

/-- If `α` is an infinite type, then `α ⊕ α` and `α` have the same cardinality. -/
theorem add_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c + c = c :=
  le_antisymm
    (by
      convert mul_le_mul_right' ((nat_lt_aleph0 2).le.trans h) c using 1
      <;> simp [two_mul, mul_eq_self h])
    (self_le_add_left c c)

Infinite Cardinal Addition Identity: $c + c = c$ for $\aleph_0 \leq c$

Informal description

For any infinite cardinal number $c$ (i.e., $\aleph_0 \leq c$), the sum $c + c$ is equal to $c$.

Cardinal.add_eq_max theorem

{a b : Cardinal} (ha : ℵ₀ ≤ a) : a + b = max a b

Full source

/-- If `α` is an infinite type, then the cardinality of `α ⊕ β` is the maximum
of the cardinalities of `α` and `β`. -/
theorem add_eq_max {a b : Cardinal} (ha : ℵ₀ ≤ a) : a + b = max a b :=
  le_antisymm
      (add_eq_self (ha.trans (le_max_left a b)) ▸
        add_le_add (le_max_left _ _) (le_max_right _ _)) <|
    max_le (self_le_add_right _ _) (self_le_add_left _ _)

Sum of Infinite Cardinal Equals Maximum: $a + b = \max(a, b)$ for $\aleph_0 \leq a$

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$) and any cardinal number $b$, the sum $a + b$ equals the maximum of $a$ and $b$.

Cardinal.add_eq_max' theorem

{a b : Cardinal} (ha : ℵ₀ ≤ b) : a + b = max a b

Full source

theorem add_eq_max' {a b : Cardinal} (ha : ℵ₀ ≤ b) : a + b = max a b := by
  rw [add_comm, max_comm, add_eq_max ha]

Sum of Infinite Cardinal Equals Maximum (Symmetric Version): $a + b = \max(a, b)$ for $\aleph_0 \leq b$

Informal description

For any infinite cardinal number $b$ (i.e., $\aleph_0 \leq b$) and any cardinal number $a$, the sum $a + b$ equals the maximum of $a$ and $b$.

Cardinal.add_mk_eq_max theorem

{α β : Type u} [Infinite α] : #α + #β = max #α #β

Full source

@[simp]
theorem add_mk_eq_max {α β : Type u} [Infinite α] : #α + #β = max #α #β :=
  add_eq_max (aleph0_le_mk α)

Sum of Cardinalities Equals Maximum for Infinite Type $\alpha$

Informal description

For any infinite type $\alpha$ and any type $\beta$ (both in the same universe), the sum of their cardinalities equals the maximum of their cardinalities, i.e., $\#\alpha + \#\beta = \max(\#\alpha, \#\beta)$.

Cardinal.add_mk_eq_max' theorem

{α β : Type u} [Infinite β] : #α + #β = max #α #β

Full source

@[simp]
theorem add_mk_eq_max' {α β : Type u} [Infinite β] : #α + #β = max #α #β :=
  add_eq_max' (aleph0_le_mk β)

Sum of Cardinalities Equals Maximum for Infinite Type $\beta$

Informal description

For any infinite type $\beta$ and any type $\alpha$ (both in the same universe), the sum of their cardinalities equals the maximum of their cardinalities, i.e., $\#\alpha + \#\beta = \max(\#\alpha, \#\beta)$.

Cardinal.add_mk_eq_self theorem

{α : Type*} [Infinite α] : #α + #α = #α

Full source

theorem add_mk_eq_self {α : Type*} [Infinite α] : #α + #α = #α := by
  simp

Self-Addition of Infinite Cardinality: $\#\alpha + \#\alpha = \#\alpha$

Informal description

For any infinite type $\alpha$, the sum of its cardinality with itself equals its cardinality, i.e., $\#\alpha + \#\alpha = \#\alpha$.

Cardinal.add_le_max theorem

(a b : Cardinal) : a + b ≤ max (max a b) ℵ₀

Full source

theorem add_le_max (a b : Cardinal) : a + b ≤ max (max a b) ℵ₀ := by
  rcases le_or_lt ℵ₀ a with ha | ha
  · rw [add_eq_max ha]
    exact le_max_left _ _
  · rcases le_or_lt ℵ₀ b with hb | hb
    · rw [add_comm, add_eq_max hb, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (add_lt_aleph0 ha hb).le

Sum of Cardinals Bounded by Maximum or Aleph-null: $a + b \leq \max(\max(a, b), \aleph_0)$

Informal description

For any two cardinal numbers $a$ and $b$, their sum satisfies $a + b \leq \max(\max(a, b), \aleph_0)$.

Cardinal.add_le_of_le theorem

{a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a ≤ c) (h2 : b ≤ c) : a + b ≤ c

Full source

theorem add_le_of_le {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a ≤ c) (h2 : b ≤ c) : a + b ≤ c :=
  (add_le_add h1 h2).trans <| le_of_eq <| add_eq_self hc

Sum of Cardinals Bounded by Infinite Cardinal

Informal description

For any cardinal numbers $a$, $b$, and $c$ such that $\aleph_0 \leq c$, if $a \leq c$ and $b \leq c$, then $a + b \leq c$.

Cardinal.add_lt_of_lt theorem

{a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b < c) : a + b < c

Full source

theorem add_lt_of_lt {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b < c) : a + b < c :=
  (add_le_add (le_max_left a b) (le_max_right a b)).trans_lt <|
    (lt_or_le (max a b) ℵ₀).elim (fun h => (add_lt_aleph0 h h).trans_le hc) fun h => by
      rw [add_eq_self h]; exact max_lt h1 h2

Sum of Cardinals Less Than Infinite Cardinal is Less Than It ($a + b < c$ when $a, b < c$ and $\aleph_0 \leq c$)

Informal description

For any cardinal numbers $a$, $b$, and $c$ such that $\aleph_0 \leq c$, if $a < c$ and $b < c$, then their sum satisfies $a + b < c$.

Cardinal.add_eq_left theorem

{a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : b ≤ a) : a + b = a

Full source

theorem add_eq_left {a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : b ≤ a) : a + b = a := by
  rw [add_eq_max ha, max_eq_left hb]

Sum of Infinite Cardinal with Smaller Cardinal: $a + b = a$ when $\aleph_0 \leq a$ and $b \leq a$

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$) and any cardinal number $b$ such that $b \leq a$, the sum $a + b$ equals $a$.

Cardinal.add_eq_right theorem

{a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a ≤ b) : a + b = b

Full source

theorem add_eq_right {a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a ≤ b) : a + b = b := by
  rw [add_comm, add_eq_left hb ha]

Sum of Smaller Cardinal with Infinite Cardinal: $a + b = b$ when $\aleph_0 \leq b$ and $a \leq b$

Informal description

For any infinite cardinal number $b$ (i.e., $\aleph_0 \leq b$) and any cardinal number $a$ such that $a \leq b$, the sum $a + b$ equals $b$.

Cardinal.add_eq_left_iff theorem

{a b : Cardinal} : a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0

Full source

theorem add_eq_left_iff {a b : Cardinal} : a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0 := by
  rw [max_le_iff]
  refine ⟨fun h => ?_, ?_⟩
  · rcases le_or_lt ℵ₀ a with ha | ha
    · left
      use ha
      rw [← not_lt]
      apply fun hb => ne_of_gt _ h
      intro hb
      exact hb.trans_le (self_le_add_left b a)
    right
    rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
    norm_cast at h ⊢
    rw [← add_right_inj, h, add_zero]
  · rintro (⟨h1, h2⟩ | h3)
    · rw [add_eq_max h1, max_eq_left h2]
    · rw [h3, add_zero]

Characterization of when $a + b = a$ for cardinals: $a + b = a \leftrightarrow \max(\aleph_0, b) \leq a \lor b = 0$

Informal description

For any two cardinal numbers $a$ and $b$, the sum $a + b$ equals $a$ if and only if either the maximum of $\aleph_0$ and $b$ is less than or equal to $a$, or $b$ is zero.

Cardinal.add_eq_right_iff theorem

{a b : Cardinal} : a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0

Full source

theorem add_eq_right_iff {a b : Cardinal} : a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0 := by
  rw [add_comm, add_eq_left_iff]

Characterization of when $a + b = b$ for cardinals: $a + b = b \leftrightarrow \max(\aleph_0, a) \leq b \lor a = 0$

Informal description

For any two cardinal numbers $a$ and $b$, the sum $a + b$ equals $b$ if and only if either the maximum of $\aleph_0$ and $a$ is less than or equal to $b$, or $a$ is zero.

Cardinal.add_nat_eq theorem

{a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : a + n = a

Full source

theorem add_nat_eq {a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : a + n = a :=
  add_eq_left ha ((nat_lt_aleph0 _).le.trans ha)

Infinite Cardinal Absorption: $a + n = a$ for $\aleph_0 \leq a$ and $n \in \mathbb{N}$

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$) and any natural number $n$, the sum $a + n$ equals $a$.

Cardinal.nat_add_eq theorem

{a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : n + a = a

Full source

theorem nat_add_eq {a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : n + a = a := by
  rw [add_comm, add_nat_eq n ha]

Infinite Cardinal Absorption: $n + a = a$ for $\aleph_0 \leq a$ and $n \in \mathbb{N}$

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$) and any natural number $n$, the sum $n + a$ equals $a$.

Cardinal.add_one_eq theorem

{a : Cardinal} (ha : ℵ₀ ≤ a) : a + 1 = a

Full source

theorem add_one_eq {a : Cardinal} (ha : ℵ₀ ≤ a) : a + 1 = a :=
  add_one_of_aleph0_le ha

Infinite Cardinal Absorption: $a + 1 = a$ for $\aleph_0 \leq a$

Informal description

For any infinite cardinal number $a$ (i.e., $\aleph_0 \leq a$), the sum of $a$ and $1$ equals $a$, i.e., $a + 1 = a$.

Cardinal.mk_add_one_eq theorem

{α : Type*} [Infinite α] : #α + 1 = #α

Full source

theorem mk_add_one_eq {α : Type*} [Infinite α] : #α + 1 = #α :=
  add_one_eq (aleph0_le_mk α)

Infinite Type Cardinal Absorption: $\#\alpha + 1 = \#\alpha$

Informal description

For any infinite type $\alpha$, the cardinality of $\alpha$ plus one equals the cardinality of $\alpha$, i.e., $\#\alpha + 1 = \#\alpha$.

Cardinal.ciSup_add theorem

(hf : BddAbove (range f)) (c : Cardinal.{v}) : (⨆ i, f i) + c = ⨆ i, f i + c

Full source

protected theorem ciSup_add (hf : BddAbove (range f)) (c : CardinalCardinal.{v}) :
    (⨆ i, f i) + c = ⨆ i, f i + c := by
  have : ∀ i, f i + c ≤ (⨆ i, f i) + c := fun i ↦ add_le_add_right (le_ciSup hf i) c
  refine le_antisymm ?_ (ciSup_le' this)
  have bdd : BddAbove (range (f · + c)) := ⟨_, forall_mem_range.mpr this⟩
  obtain hs | hs := lt_or_le (⨆ i, f i) ℵ₀
  · obtain ⟨i, hi⟩ := exists_eq_of_iSup_eq_of_not_isSuccLimit
      f hf (not_isSuccLimit_of_lt_aleph0 hs) rfl
    exact hi ▸ le_ciSup bdd i
  rw [add_eq_max hs, max_le_iff]
  exact ⟨ciSup_mono bdd fun i ↦ self_le_add_right _ c,
    (self_le_add_left _ _).trans (le_ciSup bdd <| Classical.arbitrary ι)⟩

Supremum Addition Law for Cardinal Numbers: $(\bigsqcup_i f(i)) + c = \bigsqcup_i (f(i) + c)$

Informal description

Let $\{f(i)\}_{i \in \iota}$ be a family of cardinal numbers indexed by $\iota$ whose range is bounded above. Then for any cardinal number $c$, the sum of the supremum of the family and $c$ equals the supremum of the family obtained by adding $c$ to each $f(i)$. That is, \[ \left(\bigsqcup_{i} f(i)\right) + c = \bigsqcup_{i} (f(i) + c). \]

Cardinal.add_ciSup theorem

(hf : BddAbove (range f)) (c : Cardinal.{v}) : c + (⨆ i, f i) = ⨆ i, c + f i

Full source

protected theorem add_ciSup (hf : BddAbove (range f)) (c : CardinalCardinal.{v}) :
    c + (⨆ i, f i) = ⨆ i, c + f i := by
  rw [add_comm, Cardinal.ciSup_add f hf]; simp_rw [add_comm]

Addition Commutes with Supremum in Cardinal Arithmetic: $c + (\bigsqcup_i f(i)) = \bigsqcup_i (c + f(i))$

Informal description

Let $\{f(i)\}_{i \in \iota}$ be a family of cardinal numbers indexed by $\iota$ whose range is bounded above. Then for any cardinal number $c$, the sum of $c$ and the supremum of the family equals the supremum of the family obtained by adding $c$ to each $f(i)$. That is, \[ c + \left(\bigsqcup_{i} f(i)\right) = \bigsqcup_{i} (c + f(i)). \]

Cardinal.ciSup_add_ciSup theorem

 (hf : BddAbove (range f)) (g : ι' → Cardinal.{v}) (hg : BddAbove (range g)) :
  (⨆ i, f i) + (⨆ j, g j) = ⨆ (i) (j), f i + g j

Full source

protected theorem ciSup_add_ciSup (hf : BddAbove (range f)) (g : ι' → CardinalCardinal.{v})
    (hg : BddAbove (range g)) :
    (⨆ i, f i) + (⨆ j, g j) = ⨆ (i) (j), f i + g j := by
  simp_rw [Cardinal.ciSup_add f hf, Cardinal.add_ciSup g hg]

Supremum Addition Law for Two Families of Cardinals: $(\bigsqcup_i f_i) + (\bigsqcup_j g_j) = \bigsqcup_{i,j} (f_i + g_j)$

Informal description

Let $\{f(i)\}_{i \in \iota}$ and $\{g(j)\}_{j \in \iota'}$ be two families of cardinal numbers whose ranges are bounded above. Then the sum of their suprema equals the supremum of their pairwise sums, i.e., \[ \left(\bigsqcup_{i} f(i)\right) + \left(\bigsqcup_{j} g(j)\right) = \bigsqcup_{i,j} (f(i) + g(j)). \]

Cardinal.ciSup_mul theorem

(c : Cardinal.{v}) : (⨆ i, f i) * c = ⨆ i, f i * c

Full source

protected theorem ciSup_mul (c : CardinalCardinal.{v}) : (⨆ i, f i) * c = ⨆ i, f i * c := by
  cases isEmpty_or_nonempty ι; · simp
  obtain rfl | h0 := eq_or_ne c 0; · simp
  by_cases hf : BddAbove (range f); swap
  · have hfc : ¬ BddAbove (range (f · * c)) := fun bdd ↦ hf
      ⟨⨆ i, f i * c, forall_mem_range.mpr fun i ↦ (le_mul_right h0).trans (le_ciSup bdd i)⟩
    simp [iSup, csSup_of_not_bddAbove, hf, hfc]
  have : ∀ i, f i * c ≤ (⨆ i, f i) * c := fun i ↦ mul_le_mul_right' (le_ciSup hf i) c
  refine le_antisymm ?_ (ciSup_le' this)
  have bdd : BddAbove (range (f · * c)) := ⟨_, forall_mem_range.mpr this⟩
  obtain hs | hs := lt_or_le (⨆ i, f i) ℵ₀
  · obtain ⟨i, hi⟩ := exists_eq_of_iSup_eq_of_not_isSuccLimit
      f hf (not_isSuccLimit_of_lt_aleph0 hs) rfl
    exact hi ▸ le_ciSup bdd i
  rw [mul_eq_max_of_aleph0_le_left hs h0, max_le_iff]
  obtain ⟨i, hi⟩ := exists_lt_of_lt_ciSup' (one_lt_aleph0.trans_le hs)
  exact ⟨ciSup_mono bdd fun i ↦ le_mul_right h0,
    (le_mul_left (zero_lt_one.trans hi).ne').trans (le_ciSup bdd i)⟩

Distributivity of Supremum over Multiplication in Cardinal Arithmetic: $(\bigsqcup_i f_i) \cdot c = \bigsqcup_i (f_i \cdot c)$

Informal description

For any cardinal number $c$ and any family of cardinals $\{f_i\}_{i \in \iota}$ with a bounded supremum, the product of the supremum of the family with $c$ equals the supremum of the products, i.e., \[ \left(\bigsqcup_{i} f_i\right) \cdot c = \bigsqcup_{i} (f_i \cdot c). \]

Cardinal.mul_ciSup theorem

(c : Cardinal.{v}) : c * (⨆ i, f i) = ⨆ i, c * f i

Full source

protected theorem mul_ciSup (c : CardinalCardinal.{v}) : c * (⨆ i, f i) = ⨆ i, c * f i := by
  rw [mul_comm, Cardinal.ciSup_mul f]; simp_rw [mul_comm]

Distributivity of Multiplication over Supremum in Cardinal Arithmetic: $c \cdot (\bigsqcup_i f_i) = \bigsqcup_i (c \cdot f_i)$

Informal description

For any cardinal number $c$ and any family of cardinals $\{f_i\}_{i \in \iota}$ with a bounded supremum, the product of $c$ with the supremum of the family equals the supremum of the products of $c$ with each $f_i$, i.e., \[ c \cdot \left(\bigsqcup_{i} f_i\right) = \bigsqcup_{i} (c \cdot f_i). \]

Cardinal.ciSup_mul_ciSup theorem

(g : ι' → Cardinal.{v}) : (⨆ i, f i) * (⨆ j, g j) = ⨆ (i) (j), f i * g j

Full source

protected theorem ciSup_mul_ciSup (g : ι' → CardinalCardinal.{v}) :
    (⨆ i, f i) * (⨆ j, g j) = ⨆ (i) (j), f i * g j := by
  simp_rw [Cardinal.ciSup_mul f, Cardinal.mul_ciSup g]

Product of Suprema Equals Supremum of Products in Cardinal Arithmetic: $(\bigsqcup_i f_i)(\bigsqcup_j g_j) = \bigsqcup_{i,j} f_i g_j$

Informal description

For any two families of cardinal numbers $\{f_i\}_{i \in \iota}$ and $\{g_j\}_{j \in \iota'}$, the product of their suprema equals the supremum of their pairwise products, i.e., \[ \left(\bigsqcup_{i} f_i\right) \cdot \left(\bigsqcup_{j} g_j\right) = \bigsqcup_{i,j} (f_i \cdot g_j). \]

Cardinal.sum_eq_iSup_lift theorem

{f : ι → Cardinal.{max u v}} (hι : ℵ₀ ≤ #ι) (h : lift.{v} #ι ≤ iSup f) : sum f = iSup f

Full source

theorem sum_eq_iSup_lift {f : ι → CardinalCardinal.{max u v}} (hι : ℵ₀ ≤ #ι)
    (h : lift.{v} #ι ≤ iSup f) : sum f = iSup f := by
  apply (iSup_le_sum f).antisymm'
  convert sum_le_iSup_lift f
  rw [mul_eq_max (aleph0_le_lift.mpr hι) ((aleph0_le_lift.mpr hι).trans h), max_eq_right h]

Sum of Cardinals Equals Supremum under Infinite Index Condition

Informal description

Let $\iota$ be a type in universe $u$ and $f : \iota \to \text{Cardinal}_{\max(u,v)}$ be a family of cardinal numbers. If the cardinality of $\iota$ is infinite (i.e., $\aleph_0 \leq \#\iota$) and the lifted cardinality of $\iota$ (to universe $\max(u,v)$) is less than or equal to the supremum of the family $f$, then the sum of the cardinals $f(i)$ equals their supremum. In symbols: $$\sum_{i \in \iota} f(i) = \sup_{i \in \iota} f(i)$$

Cardinal.sum_eq_iSup theorem

{f : ι → Cardinal.{u}} (hι : ℵ₀ ≤ #ι) (h : #ι ≤ iSup f) : sum f = iSup f

Full source

theorem sum_eq_iSup {f : ι → CardinalCardinal.{u}} (hι : ℵ₀ ≤ #ι) (h : #ι ≤ iSup f) : sum f = iSup f :=
  sum_eq_iSup_lift hι ((lift_id #ι).symm ▸ h)

Sum of Cardinals Equals Supremum under Infinite Index Condition (Unlifted Version)

Informal description

Let $\iota$ be a type and $f : \iota \to \text{Cardinal}$ be a family of cardinal numbers. If the cardinality of $\iota$ is infinite (i.e., $\aleph_0 \leq \#\iota$) and the cardinality of $\iota$ is less than or equal to the supremum of the family $f$, then the sum of the cardinals $f(i)$ equals their supremum. In symbols: $$\sum_{i \in \iota} f(i) = \sup_{i \in \iota} f(i)$$

Cardinal.aleph_add_aleph theorem

(o₁ o₂ : Ordinal) : ℵ_ o₁ + ℵ_ o₂ = ℵ_ (max o₁ o₂)

Full source

@[simp]
theorem aleph_add_aleph (o₁ o₂ : Ordinal) : ℵ_ o₁ + ℵ_ o₂ = ℵ_ (max o₁ o₂) := by
  rw [Cardinal.add_eq_max (aleph0_le_aleph o₁), aleph_max]

Sum of Aleph Numbers Equals Aleph of Maximum: $\aleph_{o_1} + \aleph_{o_2} = \aleph_{\max(o_1, o_2)}$

Informal description

For any two ordinals $o_1$ and $o_2$, the sum of the corresponding aleph numbers $\aleph_{o_1} + \aleph_{o_2}$ equals the aleph number indexed by the maximum of $o_1$ and $o_2$, i.e., \[ \aleph_{o_1} + \aleph_{o_2} = \aleph_{\max(o_1, o_2)}. \]

Cardinal.add_right_inj_of_lt_aleph0 theorem

{α β γ : Cardinal} (γ₀ : γ < aleph0) : α + γ = β + γ ↔ α = β

Full source

theorem add_right_inj_of_lt_aleph0 {α β γ : Cardinal} (γ₀ : γ < aleph0) : α + γ = β + γ ↔ α = β :=
  ⟨fun h => Cardinal.eq_of_add_eq_add_right h γ₀, fun h => congr_arg (· + γ) h⟩

Right Cancellation Law for Cardinal Addition with Finite $\gamma$

Informal description

For any cardinal numbers $\alpha$, $\beta$, and $\gamma$, if $\gamma$ is strictly less than $\aleph_0$, then $\alpha + \gamma = \beta + \gamma$ if and only if $\alpha = \beta$.

Cardinal.add_nat_inj theorem

{α β : Cardinal} (n : ℕ) : α + n = β + n ↔ α = β

Full source

@[simp]
theorem add_nat_inj {α β : Cardinal} (n : ℕ) : α + n = β + n ↔ α = β :=
  add_right_inj_of_lt_aleph0 (nat_lt_aleph0 _)

Right Cancellation Law for Cardinal Addition with Natural Numbers

Informal description

For any cardinal numbers $\alpha$ and $\beta$ and any natural number $n$, the equality $\alpha + n = \beta + n$ holds if and only if $\alpha = \beta$.

Cardinal.add_one_inj theorem

{α β : Cardinal} : α + 1 = β + 1 ↔ α = β

Full source

@[simp]
theorem add_one_inj {α β : Cardinal} : α + 1 = β + 1 ↔ α = β :=
  add_right_inj_of_lt_aleph0 one_lt_aleph0

Right Cancellation Law for Cardinal Addition with One: $\alpha + 1 = \beta + 1 \leftrightarrow \alpha = \beta$

Informal description

For any cardinal numbers $\alpha$ and $\beta$, the equality $\alpha + 1 = \beta + 1$ holds if and only if $\alpha = \beta$.

Cardinal.add_le_add_iff_of_lt_aleph0 theorem

{α β γ : Cardinal} (γ₀ : γ < ℵ₀) : α + γ ≤ β + γ ↔ α ≤ β

Full source

theorem add_le_add_iff_of_lt_aleph0 {α β γ : Cardinal} (γ₀ : γ < ℵ₀) :
    α + γ ≤ β + γ ↔ α ≤ β := by
  refine ⟨fun h => ?_, fun h => add_le_add_right h γ⟩
  contrapose h
  rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢
  exact ⟨add_le_add_right h.1 γ, mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩

Inequality Preservation under Cardinal Addition with Finite $\gamma$

Informal description

For any cardinal numbers $\alpha$, $\beta$, and $\gamma$, if $\gamma$ is strictly less than $\aleph_0$, then $\alpha + \gamma \leq \beta + \gamma$ if and only if $\alpha \leq \beta$.

Cardinal.add_nat_le_add_nat_iff theorem

{α β : Cardinal} (n : ℕ) : α + n ≤ β + n ↔ α ≤ β

Full source

@[simp]
theorem add_nat_le_add_nat_iff {α β : Cardinal} (n : ℕ) : α + n ≤ β + n ↔ α ≤ β :=
  add_le_add_iff_of_lt_aleph0 (nat_lt_aleph0 n)

Inequality Preservation under Cardinal Addition with Natural Numbers: $\alpha + n \leq \beta + n \leftrightarrow \alpha \leq \beta$

Informal description

For any cardinal numbers $\alpha$ and $\beta$ and any natural number $n$, the inequality $\alpha + n \leq \beta + n$ holds if and only if $\alpha \leq \beta$.

Cardinal.add_one_le_add_one_iff theorem

{α β : Cardinal} : α + 1 ≤ β + 1 ↔ α ≤ β

Full source

@[simp]
theorem add_one_le_add_one_iff {α β : Cardinal} : α + 1 ≤ β + 1 ↔ α ≤ β :=
  add_le_add_iff_of_lt_aleph0 one_lt_aleph0

Inequality Preservation under Cardinal Addition of One: $\alpha + 1 \leq \beta + 1 \leftrightarrow \alpha \leq \beta$

Informal description

For any two cardinal numbers $\alpha$ and $\beta$, the inequality $\alpha + 1 \leq \beta + 1$ holds if and only if $\alpha \leq \beta$.

Cardinal.pow_le theorem

{κ μ : Cardinal.{u}} (H1 : ℵ₀ ≤ κ) (H2 : μ < ℵ₀) : κ ^ μ ≤ κ

Full source

theorem pow_le {κ μ : CardinalCardinal.{u}} (H1 : ℵ₀ ≤ κ) (H2 : μ < ℵ₀) : κ ^ μ ≤ κ :=
  let ⟨n, H3⟩ := lt_aleph0.1 H2
  H3.symm ▸
    Quotient.inductionOn κ
      (fun α H1 =>
        Nat.recOn n
          (lt_of_lt_of_le
              (by
                rw [Nat.cast_zero, power_zero]
                exact one_lt_aleph0)
              H1).le
          fun n ih =>
          le_of_le_of_eq
            (by
              rw [Nat.cast_succ, power_add, power_one]
              exact mul_le_mul_right' ih _)
            (mul_eq_self H1))
      H1

Bound on Exponentiation of Infinite Cardinal by Finite Cardinal: $\kappa^\mu \leq \kappa$ for $\aleph_0 \leq \kappa$ and $\mu < \aleph_0$

Informal description

For any infinite cardinal $\kappa$ (i.e., $\aleph_0 \leq \kappa$) and any finite cardinal $\mu$ (i.e., $\mu < \aleph_0$), the cardinal exponentiation $\kappa^\mu$ satisfies $\kappa^\mu \leq \kappa$.

Cardinal.pow_eq theorem

{κ μ : Cardinal.{u}} (H1 : ℵ₀ ≤ κ) (H2 : 1 ≤ μ) (H3 : μ < ℵ₀) : κ ^ μ = κ

Full source

theorem pow_eq {κ μ : CardinalCardinal.{u}} (H1 : ℵ₀ ≤ κ) (H2 : 1 ≤ μ) (H3 : μ < ℵ₀) : κ ^ μ = κ :=
  (pow_le H1 H3).antisymm <| self_le_power κ H2

Exponentiation of Infinite Cardinal by Finite Cardinal: $\kappa^\mu = \kappa$ for $\aleph_0 \leq \kappa$ and $1 \leq \mu < \aleph_0$

Informal description

For any infinite cardinal $\kappa$ (i.e., $\aleph_0 \leq \kappa$) and any nonzero finite cardinal $\mu$ (i.e., $1 \leq \mu < \aleph_0$), the cardinal exponentiation satisfies $\kappa^\mu = \kappa$.

Cardinal.power_self_eq theorem

{c : Cardinal} (h : ℵ₀ ≤ c) : c ^ c = 2 ^ c

Full source

theorem power_self_eq {c : Cardinal} (h : ℵ₀ ≤ c) : c ^ c = 2 ^ c := by
  apply ((power_le_power_right <| (cantor c).le).trans _).antisymm
  · exact power_le_power_right ((nat_lt_aleph0 2).le.trans h)
  · rw [← power_mul, mul_eq_self h]

Cardinal Exponentiation Identity: $c^c = 2^c$ for Infinite Cardinals

Informal description

For any infinite cardinal number $c$ (i.e., $\aleph_0 \leq c$), the cardinal exponentiation $c^c$ equals $2^c$.

Cardinal.prod_eq_two_power theorem

 {ι : Type u} [Infinite ι] {c : ι → Cardinal.{v}} (h₁ : ∀ i, 2 ≤ c i) (h₂ : ∀ i, lift.{u} (c i) ≤ lift.{v} #ι) :
  prod c = 2 ^ lift.{v} #ι

Full source

theorem prod_eq_two_power {ι : Type u} [Infinite ι] {c : ι → CardinalCardinal.{v}} (h₁ : ∀ i, 2 ≤ c i)
    (h₂ : ∀ i, lift.{u} (c i) ≤ lift.{v} #ι) : prod c = 2 ^ lift.{v} #ι := by
  rw [← lift_id'.{u, v} (prod.{u, v} c), lift_prod, ← lift_two_power]
  apply le_antisymm
  · refine (prod_le_prod _ _ h₂).trans_eq ?_
    rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umaxlift_umax.{u, v}]
  · rw [← prod_const', lift_prod]
    refine prod_le_prod _ _ fun i => ?_
    rw [lift_two, ← lift_twolift_two.{u, v}, lift_le]
    exact h₁ i

Product of Cardinals Equals Two to the Power of Cardinality for Infinite Index Set

Informal description

Let $\iota$ be an infinite type, and let $\{c_i\}_{i \in \iota}$ be a family of cardinal numbers such that for each $i \in \iota$, $2 \leq c_i$ and the lift of $c_i$ is at most the lift of the cardinality of $\iota$. Then the product of the cardinals $c_i$ equals $2$ raised to the power of the lift of the cardinality of $\iota$, i.e., \[ \prod_{i \in \iota} c_i = 2^{\text{lift}(\#\iota)}. \]

Cardinal.power_eq_two_power theorem

{c₁ c₂ : Cardinal} (h₁ : ℵ₀ ≤ c₁) (h₂ : 2 ≤ c₂) (h₂' : c₂ ≤ c₁) : c₂ ^ c₁ = 2 ^ c₁

Full source

theorem power_eq_two_power {c₁ c₂ : Cardinal} (h₁ : ℵ₀ ≤ c₁) (h₂ : 2 ≤ c₂) (h₂' : c₂ ≤ c₁) :
    c₂ ^ c₁ = 2 ^ c₁ :=
  le_antisymm (power_self_eq h₁ ▸ power_le_power_right h₂') (power_le_power_right h₂)

Cardinal Exponentiation Identity: $c_2^{c_1} = 2^{c_1}$ for Infinite $c_1$ and $2 \leq c_2 \leq c_1$

Informal description

For any infinite cardinal number $c_1$ (i.e., $\aleph_0 \leq c_1$) and any cardinal number $c_2$ such that $2 \leq c_2 \leq c_1$, the cardinal exponentiation $c_2^{c_1}$ equals $2^{c_1}$.

Cardinal.nat_power_eq theorem

{c : Cardinal.{u}} (h : ℵ₀ ≤ c) {n : ℕ} (hn : 2 ≤ n) : (n : Cardinal.{u}) ^ c = 2 ^ c

Full source

theorem nat_power_eq {c : CardinalCardinal.{u}} (h : ℵ₀ ≤ c) {n : ℕ} (hn : 2 ≤ n) :
    (n : CardinalCardinal.{u}) ^ c = 2 ^ c :=
  power_eq_two_power h (by assumption_mod_cast) ((nat_lt_aleph0 n).le.trans h)

Cardinal Exponentiation Identity: $n^\kappa = 2^\kappa$ for Infinite $\kappa$ and $n \geq 2$

Informal description

For any infinite cardinal number $\kappa$ (i.e., $\aleph_0 \leq \kappa$) and any natural number $n \geq 2$, the cardinal exponentiation $n^\kappa$ equals $2^\kappa$.

Cardinal.power_nat_le theorem

{c : Cardinal.{u}} {n : ℕ} (h : ℵ₀ ≤ c) : c ^ n ≤ c

Full source

theorem power_nat_le {c : CardinalCardinal.{u}} {n : ℕ} (h : ℵ₀ ≤ c) : c ^ n ≤ c :=
  pow_le h (nat_lt_aleph0 n)

Exponentiation of Infinite Cardinal by Natural Number: $\kappa^n \leq \kappa$ for $\aleph_0 \leq \kappa$

Informal description

For any infinite cardinal $\kappa$ (i.e., $\aleph_0 \leq \kappa$) and any natural number $n$, the cardinal exponentiation $\kappa^n$ satisfies $\kappa^n \leq \kappa$.

Cardinal.power_nat_eq theorem

{c : Cardinal.{u}} {n : ℕ} (h1 : ℵ₀ ≤ c) (h2 : 1 ≤ n) : c ^ n = c

Full source

theorem power_nat_eq {c : CardinalCardinal.{u}} {n : ℕ} (h1 : ℵ₀ ≤ c) (h2 : 1 ≤ n) : c ^ n = c :=
  pow_eq h1 (mod_cast h2) (nat_lt_aleph0 n)

Exponentiation of Infinite Cardinal by Natural Number: $\kappa^n = \kappa$ for $\aleph_0 \leq \kappa$ and $1 \leq n$

Informal description

For any infinite cardinal $\kappa$ (i.e., $\aleph_0 \leq \kappa$) and any positive natural number $n$ (i.e., $1 \leq n$), the cardinal exponentiation satisfies $\kappa^n = \kappa$.

Cardinal.power_nat_le_max theorem

{c : Cardinal.{u}} {n : ℕ} : c ^ (n : Cardinal.{u}) ≤ max c ℵ₀

Full source

theorem power_nat_le_max {c : CardinalCardinal.{u}} {n : ℕ} : c ^ (n : CardinalCardinal.{u}) ≤ max c ℵ₀ := by
  rcases le_or_lt ℵ₀ c with hc | hc
  · exact le_max_of_le_left (power_nat_le hc)
  · exact le_max_of_le_right (power_lt_aleph0 hc (nat_lt_aleph0 _)).le

Bound on Cardinal Exponentiation: $c^n \leq \max(c, \aleph_0)$

Informal description

For any cardinal number $c$ and any natural number $n$, the cardinal exponentiation $c^n$ satisfies $c^n \leq \max(c, \aleph_0)$.

Cardinal.power_le_aleph0 theorem

{a b : Cardinal.{u}} (ha : a ≤ ℵ₀) (hb : b < ℵ₀) : a ^ b ≤ ℵ₀

Full source

lemma power_le_aleph0 {a b : CardinalCardinal.{u}} (ha : a ≤ ℵ₀) (hb : b < ℵ₀) : a ^ b ≤ ℵ₀ := by
  lift b to ℕ using hb; simpa [ha] using power_nat_le_max (c := a)

Bound on Exponentiation of Cardinals Below $\aleph_0$: $a^b \leq \aleph_0$ when $a \leq \aleph_0$ and $b < \aleph_0$

Informal description

For any cardinal numbers $a$ and $b$ such that $a \leq \aleph_0$ and $b < \aleph_0$, the cardinal exponentiation $a^b$ satisfies $a^b \leq \aleph_0$.

Cardinal.powerlt_aleph0 theorem

{c : Cardinal} (h : ℵ₀ ≤ c) : c ^< ℵ₀ = c

Full source

theorem powerlt_aleph0 {c : Cardinal} (h : ℵ₀ ≤ c) : c ^< ℵ₀ = c := by
  apply le_antisymm
  · rw [powerlt_le]
    intro c'
    rw [lt_aleph0]
    rintro ⟨n, rfl⟩
    apply power_nat_le h
  convert le_powerlt c one_lt_aleph0; rw [power_one]

Supremum of finite powers of infinite cardinal: $c^{<\aleph_0} = c$

Informal description

For any infinite cardinal number $c$ (i.e., $\aleph_0 \leq c$), the supremum of $c^n$ over all natural numbers $n$ is equal to $c$ itself, i.e., $c^{<\aleph_0} = c$.

Cardinal.powerlt_aleph0_le theorem

(c : Cardinal) : c ^< ℵ₀ ≤ max c ℵ₀

Full source

theorem powerlt_aleph0_le (c : Cardinal) : c ^< ℵ₀ ≤ max c ℵ₀ := by
  rcases le_or_lt ℵ₀ c with h | h
  · rw [powerlt_aleph0 h]
    apply le_max_left
  rw [powerlt_le]
  exact fun c' hc' => (power_lt_aleph0 h hc').le.trans (le_max_right _ _)

Bound on finite powers: $c^{<\aleph_0} \leq \max(c, \aleph_0)$

Informal description

For any cardinal number $c$, the supremum of $c^n$ over all natural numbers $n$ (denoted $c^{<\aleph_0}$) is less than or equal to the maximum of $c$ and $\aleph_0$, i.e., $c^{<\aleph_0} \leq \max(c, \aleph_0)$.

Cardinal.mk_equiv_eq_zero_iff_lift_ne theorem

: #(α ≃ β') = 0 ↔ lift.{v} #α ≠ lift.{u} #β'

Full source

theorem mk_equiv_eq_zero_iff_lift_ne : #(α ≃ β')#(α ≃ β') = 0 ↔ lift.{v} #α ≠ lift.{u} #β' := by
  rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_eq']

Zero Cardinality of Bijections is Equivalent to Unequal Lifted Cardinalities

Informal description

For any types $\alpha$ in universe $u$ and $\beta'$ in universe $v$, the cardinality of the set of bijections between $\alpha$ and $\beta'$ is zero if and only if the lifted cardinality of $\alpha$ (to universe $v$) is not equal to the lifted cardinality of $\beta'$ (to universe $u$). In other words, $\#(\alpha \simeq \beta') = 0 \leftrightarrow \text{lift}_v \#\alpha \neq \text{lift}_u \#\beta'$.

Cardinal.mk_equiv_eq_zero_iff_ne theorem

: #(α ≃ β) = 0 ↔ #α ≠ #β

Full source

theorem mk_equiv_eq_zero_iff_ne : #(α ≃ β)#(α ≃ β) = 0 ↔ #α ≠ #β := by
  rw [mk_equiv_eq_zero_iff_lift_ne, lift_id, lift_id]

Zero Bijection Cardinality Criterion: $\#(\alpha \simeq \beta) = 0 \leftrightarrow \#\alpha \neq \#\beta$

Informal description

For any types $\alpha$ and $\beta$, the cardinality of the set of bijections between $\alpha$ and $\beta$ is zero if and only if the cardinality of $\alpha$ is not equal to the cardinality of $\beta$. In other words, $\#(\alpha \simeq \beta) = 0 \leftrightarrow \#\alpha \neq \#\beta$.

Cardinal.mk_equiv_comm theorem

: #(α ≃ β') = #(β' ≃ α)

Full source

/-- This lemma makes lemmas assuming `Infinite α` applicable to the situation where we have
  `Infinite β` instead. -/
theorem mk_equiv_comm : #(α ≃ β') = #(β' ≃ α) :=
  (ofBijective _ symm_bijective).cardinal_eq

Cardinality of Equivalence Sets is Symmetric

Informal description

For any types $\alpha$ and $\beta'$, the cardinality of the set of equivalences (bijections) from $\alpha$ to $\beta'$ is equal to the cardinality of the set of equivalences from $\beta'$ to $\alpha$. In other words, $\#(\alpha \simeq \beta') = \#(\beta' \simeq \alpha)$.

Cardinal.mk_embedding_eq_zero_iff_lift_lt theorem

: #(α ↪ β') = 0 ↔ lift.{u} #β' < lift.{v} #α

Full source

theorem mk_embedding_eq_zero_iff_lift_lt : #(α ↪ β')#(α ↪ β') = 0 ↔ lift.{u} #β' < lift.{v} #α := by
  rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_le', not_le]

Zero Embedding Cardinality Criterion via Lifted Cardinalities

Informal description

For any types $\alpha$ and $\beta'$, the cardinality of the set of embeddings from $\alpha$ to $\beta'$ is zero if and only if the lift of the cardinality of $\beta'$ (to universe level $u$) is strictly less than the lift of the cardinality of $\alpha$ (to universe level $v$). In other words, $\#(\alpha \hookrightarrow \beta') = 0$ if and only if $\text{lift}_{u}(\#\beta') < \text{lift}_{v}(\#\alpha)$.

Cardinal.mk_embedding_eq_zero_iff_lt theorem

: #(α ↪ β) = 0 ↔ #β < #α

Full source

theorem mk_embedding_eq_zero_iff_lt : #(α ↪ β)#(α ↪ β) = 0 ↔ #β < #α := by
  rw [mk_embedding_eq_zero_iff_lift_lt, lift_lt]

Zero Embedding Cardinality Criterion: $\#(\alpha \hookrightarrow \beta) = 0 \leftrightarrow \#\beta < \#\alpha$

Informal description

For any types $\alpha$ and $\beta$, the cardinality of the set of embeddings from $\alpha$ to $\beta$ is zero if and only if the cardinality of $\beta$ is strictly less than the cardinality of $\alpha$. In other words, $\#(\alpha \hookrightarrow \beta) = 0 \leftrightarrow \#\beta < \#\alpha$.

Cardinal.mk_arrow_eq_zero_iff theorem

: #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0

Full source

theorem mk_arrow_eq_zero_iff : #(α → β')#(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0 := by
  simp_rw [mk_eq_zero_iff, mk_ne_zero_iff, isEmpty_fun]

Cardinality of Function Space is Zero if and only if Domain is Nonempty and Codomain is Empty

Informal description

The set of all functions from a type $\alpha$ to a type $\beta'$ has cardinality zero if and only if $\alpha$ is nonempty and $\beta'$ is empty. In other words, $\#(\alpha \to \beta') = 0$ if and only if $\#\alpha \neq 0$ and $\#\beta' = 0$.

Cardinal.mk_surjective_eq_zero_iff_lift theorem

: #{f : α → β' | Surjective f} = 0 ↔ lift.{v} #α < lift.{u} #β' ∨ (#α ≠ 0 ∧ #β' = 0)

Full source

theorem mk_surjective_eq_zero_iff_lift :
    #{f : α → β' | Surjective f}#{f : α → β' | Surjective f} = 0 ↔ lift.{v} #α < lift.{u} #β' ∨ (#α ≠ 0 ∧ #β' = 0) := by
  rw [← not_iff_not, not_or, not_lt, lift_mk_le', ← Ne, not_and_or, not_ne_iff, and_comm]
  simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]

Characterization of When No Surjective Functions Exist Between Types

Informal description

Let $\alpha$ and $\beta'$ be types with cardinalities $\#\alpha$ and $\#\beta'$ respectively. The set of surjective functions from $\alpha$ to $\beta'$ is empty if and only if either: 1. The lift of $\#\alpha$ (to a higher universe) is strictly less than the lift of $\#\beta'$, or 2. $\alpha$ is nonempty ($\#\alpha \neq 0$) and $\beta'$ is empty ($\#\beta' = 0$). In symbols: \[ \#\{f : \alpha \to \beta' \mid \text{Surjective } f\} = 0 \leftrightarrow \text{lift}(\#\alpha) < \text{lift}(\#\beta') \lor (\#\alpha \neq 0 \land \#\beta' = 0) \]

Cardinal.mk_surjective_eq_zero_iff theorem

: #{f : α → β | Surjective f} = 0 ↔ #α < #β ∨ (#α ≠ 0 ∧ #β = 0)

Full source

theorem mk_surjective_eq_zero_iff :
    #{f : α → β | Surjective f}#{f : α → β | Surjective f} = 0 ↔ #α < #β ∨ (#α ≠ 0 ∧ #β = 0) := by
  rw [mk_surjective_eq_zero_iff_lift, lift_lt]

Characterization of Empty Surjective Function Space: $\#\{f : \alpha \to \beta \mid \text{surjective } f\} = 0 \leftrightarrow \#\alpha < \#\beta \lor (\#\alpha \neq 0 \land \#\beta = 0)$

Informal description

For any types $\alpha$ and $\beta$, the set of surjective functions from $\alpha$ to $\beta$ is empty if and only if either: 1. The cardinality of $\alpha$ is strictly less than the cardinality of $\beta$, or 2. $\alpha$ is nonempty ($\#\alpha \neq 0$) and $\beta$ is empty ($\#\beta = 0$). In symbols: \[ \#\{f : \alpha \to \beta \mid f \text{ is surjective}\} = 0 \leftrightarrow \#\alpha < \#\beta \lor (\#\alpha \neq 0 \land \#\beta = 0) \]

Cardinal.mk_equiv_le_embedding theorem

: #(α ≃ β') ≤ #(α ↪ β')

Full source

theorem mk_equiv_le_embedding : #(α ≃ β') ≤ #(α ↪ β') := ⟨⟨_, Equiv.toEmbedding_injective⟩⟩

Cardinality of Bijections Bounded by Cardinality of Injections

Informal description

For any types $\alpha$ and $\beta'$, the cardinality of the set of bijections (equivalences) between $\alpha$ and $\beta'$ is less than or equal to the cardinality of the set of injective functions from $\alpha$ to $\beta'$. In symbols: \[ \#(\alpha \simeq \beta') \leq \#(\alpha \hookrightarrow \beta') \]

Cardinal.mk_embedding_le_arrow theorem

: #(α ↪ β') ≤ #(α → β')

Full source

theorem mk_embedding_le_arrow : #(α ↪ β') ≤ #(α → β') := ⟨⟨_, DFunLike.coe_injective⟩⟩

Cardinality of Injections Bounded by Cardinality of All Functions

Informal description

For any types $\alpha$ and $\beta$, the cardinality of the set of injective functions from $\alpha$ to $\beta$ is less than or equal to the cardinality of the set of all functions from $\alpha$ to $\beta$. In symbols: \[ \#(\alpha \hookrightarrow \beta) \leq \#(\alpha \to \beta) \]

Cardinal.mk_perm_eq_self_power theorem

: #(Equiv.Perm α) = #α ^ #α

Full source

theorem mk_perm_eq_self_power : #(Equiv.Perm α) = #α ^ #α :=
  ((mk_equiv_le_embedding α α).trans (mk_embedding_le_arrow α α)).antisymm <| by
    suffices Nonempty ((α → Bool) ↪ Equiv.Perm (α × Bool)) by
      obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by
        erw [← Cardinal.eq, mk_prod, lift_uzero, mk_bool,
          lift_natCast, mul_two, add_eq_self (aleph0_le_mk α)]
      erw [← le_def, mk_arrow, lift_uzero, mk_bool, lift_natCast 2] at this
      rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]
    refine ⟨⟨fun f ↦ Involutive.toPerm (fun x ↦ ⟨x.1, xor (f x.1) x.2⟩) fun x ↦ ?_, fun f g h ↦ ?_⟩⟩
    · simp_rw [← Bool.xor_assoc, Bool.xor_self, Bool.false_xor]
    · ext a; rw [← (f a).xor_false, ← (g a).xor_false]; exact congr(($h ⟨a, false⟩).2)

Cardinality of Permutations: $\#(\text{Perm}(\alpha)) = \#\alpha^{\#\alpha}$

Informal description

For any type $\alpha$, the cardinality of the set of permutations (bijective self-maps) of $\alpha$ equals the cardinality of $\alpha$ raised to the power of itself, i.e., $\#(\text{Perm}(\alpha)) = \#\alpha^{\#\alpha}$.

Cardinal.mk_perm_eq_two_power theorem

: #(Equiv.Perm α) = 2 ^ #α

Full source

theorem mk_perm_eq_two_power : #(Equiv.Perm α) = 2 ^ #α := by
  rw [mk_perm_eq_self_power, power_self_eq (aleph0_le_mk α)]

Cardinality of Permutations: $\#(\text{Perm}(\alpha)) = 2^{\#\alpha}$

Informal description

For any type $\alpha$, the cardinality of the set of permutations (bijective self-maps) of $\alpha$ equals $2$ raised to the power of the cardinality of $\alpha$, i.e., $\#(\text{Perm}(\alpha)) = 2^{\#\alpha}$.

Cardinal.mk_equiv_eq_arrow_of_lift_eq theorem

(leq : lift.{v} #α = lift.{u} #β') : #(α ≃ β') = #(α → β')

Full source

theorem mk_equiv_eq_arrow_of_lift_eq (leq : lift.{v} #α = lift.{u} #β') :
    #(α ≃ β') = #(α → β') := by
  obtain ⟨e⟩ := lift_mk_eq'.mp leq
  have e₁ := lift_mk_eq'.mpr ⟨.equivCongr (.refl α) e⟩
  have e₂ := lift_mk_eq'.mpr ⟨.arrowCongr (.refl α) e⟩
  rw [lift_id'lift_id'.{u,v}] at e₁ e₂
  rw [← e₁, ← e₂, lift_inj, mk_perm_eq_self_power, power_def]

Cardinality of Equivalences Equals Cardinality of Function Space under Lifted Cardinal Equality

Informal description

For any types $\alpha$ in universe $u$ and $\beta'$ in universe $v$, if the lifted cardinalities satisfy $\text{lift}_v \#\alpha = \text{lift}_u \#\beta'$, then the cardinality of the set of equivalences (bijections) between $\alpha$ and $\beta'$ is equal to the cardinality of the function space $\alpha \to \beta'$, i.e., $\#(\alpha \simeq \beta') = \#(\alpha \to \beta')$.

Cardinal.mk_equiv_eq_arrow_of_eq theorem

(eq : #α = #β) : #(α ≃ β) = #(α → β)

Full source

theorem mk_equiv_eq_arrow_of_eq (eq : #α = #β) : #(α ≃ β) = #(α → β) :=
  mk_equiv_eq_arrow_of_lift_eq congr(lift $eq)

Cardinality of Bijections Equals Cardinality of Function Space for Equinumerous Types

Informal description

For any types $\alpha$ and $\beta$ with the same cardinality (i.e., $\#\alpha = \#\beta$), the cardinality of the set of bijections between $\alpha$ and $\beta$ equals the cardinality of the function space from $\alpha$ to $\beta$, i.e., $\#(\alpha \simeq \beta) = \#(\alpha \to \beta)$.

Cardinal.mk_equiv_of_lift_eq theorem

(leq : lift.{v} #α = lift.{u} #β') : #(α ≃ β') = 2 ^ lift.{v} #α

Full source

theorem mk_equiv_of_lift_eq (leq : lift.{v} #α = lift.{u} #β') : #(α ≃ β') = 2 ^ lift.{v} #α := by
  erw [← (lift_mk_eq'.2 ⟨.equivCongr (.refl α) (lift_mk_eq'.1 leq).some⟩).trans (lift_id'.{u,v} _),
    lift_umax.{u,v}, mk_perm_eq_two_power, lift_power, lift_natCast]; rfl

Cardinality of Bijections: $\#(\alpha \simeq \beta') = 2^{\text{lift} \#\alpha}$ under Lifted Cardinal Equality

Informal description

For any types $\alpha$ in universe $u$ and $\beta'$ in universe $v$, if the lifted cardinalities satisfy $\text{lift}_v \#\alpha = \text{lift}_u \#\beta'$, then the cardinality of the set of bijections between $\alpha$ and $\beta'$ is equal to $2$ raised to the power of $\text{lift}_v \#\alpha$, i.e., $\#(\alpha \simeq \beta') = 2^{\text{lift}_v \#\alpha}$.

Cardinal.mk_equiv_of_eq theorem

(eq : #α = #β) : #(α ≃ β) = 2 ^ #α

Full source

theorem mk_equiv_of_eq (eq : #α = #β) : #(α ≃ β) = 2 ^ #α := by
  rw [mk_equiv_of_lift_eq (lift_inj.mpr eq), lift_id]

Cardinality of Bijections: $\#(\alpha \simeq \beta) = 2^{\#\alpha}$ for Equinumerous Types

Informal description

For any types $\alpha$ and $\beta$ with the same cardinality (i.e., $\#\alpha = \#\beta$), the cardinality of the set of bijections between $\alpha$ and $\beta$ is equal to $2$ raised to the power of $\#\alpha$, i.e., $\#(\alpha \simeq \beta) = 2^{\#\alpha}$.

Cardinal.mk_embedding_eq_arrow_of_lift_le theorem

(lle : lift.{u} #β' ≤ lift.{v} #α) : #(β' ↪ α) = #(β' → α)

Full source

theorem mk_embedding_eq_arrow_of_lift_le (lle : lift.{u} #β' ≤ lift.{v} #α) :
    #(β' ↪ α) = #(β' → α) :=
  (mk_embedding_le_arrow _ _).antisymm <| by
    conv_rhs => rw [← (Equiv.embeddingCongr (.refl _)
      (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]
    obtain ⟨e⟩ := lift_mk_le'.mp lle
    exact ⟨⟨fun f ↦ ⟨fun b ↦ ⟨e b, f b⟩, fun _ _ h ↦ e.injective congr(Prod.fst $h)⟩,
      fun f g h ↦ funext fun b ↦ congr(Prod.snd <| $h b)⟩⟩

Cardinality of Injections Equals Cardinality of All Functions under Lift Condition

Informal description

For any types $\alpha$ and $\beta'$, if the lift of the cardinality of $\beta'$ is less than or equal to the lift of the cardinality of $\alpha$, then the cardinality of the set of injective functions from $\beta'$ to $\alpha$ equals the cardinality of the set of all functions from $\beta'$ to $\alpha$. In symbols: \[ \#(\beta' \hookrightarrow \alpha) = \#(\beta' \to \alpha) \]

Cardinal.mk_embedding_eq_arrow_of_le theorem

(le : #β ≤ #α) : #(β ↪ α) = #(β → α)

Full source

theorem mk_embedding_eq_arrow_of_le (le : #β ≤ #α) : #(β ↪ α) = #(β → α) :=
  mk_embedding_eq_arrow_of_lift_le (lift_le.mpr le)

Cardinality of Injections Equals Cardinality of All Functions under Cardinality Condition

Informal description

For any types $\alpha$ and $\beta$, if the cardinality of $\beta$ is less than or equal to the cardinality of $\alpha$, then the cardinality of the set of injective functions from $\beta$ to $\alpha$ equals the cardinality of the set of all functions from $\beta$ to $\alpha$. In symbols: \[ \#(\beta \hookrightarrow \alpha) = \#(\beta \to \alpha) \]

Cardinal.mk_surjective_eq_arrow_of_lift_le theorem

(lle : lift.{u} #β' ≤ lift.{v} #α) : #{f : α → β' | Surjective f} = #(α → β')

Full source

theorem mk_surjective_eq_arrow_of_lift_le (lle : lift.{u} #β' ≤ lift.{v} #α) :
    #{f : α → β' | Surjective f} = #(α → β') :=
  (mk_set_le _).antisymm <|
    have ⟨e⟩ : Nonempty (α ≃ α ⊕ β') := by
      simp_rw [← lift_mk_eq', mk_sum, lift_add, lift_lift]; rw [lift_umaxlift_umax.{u,v}, eq_comm]
      exact add_eq_left (aleph0_le_lift.mpr <| aleph0_le_mk α) lle
    ⟨⟨fun f ↦ ⟨fun a ↦ (e a).elim f id, fun b ↦ ⟨e.symm (.inr b), congr_arg _ (e.right_inv _)⟩⟩,
      fun f g h ↦ funext fun a ↦ by
        simpa only [e.apply_symm_apply] using congr_fun (Subtype.ext_iff.mp h) (e.symm <| .inl a)⟩⟩

Cardinality of Surjective Functions Equals Cardinality of All Functions under Lift Condition

Informal description

For any types $\alpha$ and $\beta'$, if the lift of the cardinality of $\beta'$ is less than or equal to the lift of the cardinality of $\alpha$, then the cardinality of the set of surjective functions from $\alpha$ to $\beta'$ equals the cardinality of the set of all functions from $\alpha$ to $\beta'$. In symbols: \[ \#\{f : \alpha \to \beta' \mid \text{Surjective } f\} = \#(\alpha \to \beta') \]

Cardinal.mk_surjective_eq_arrow_of_le theorem

(le : #β ≤ #α) : #{f : α → β | Surjective f} = #(α → β)

Full source

theorem mk_surjective_eq_arrow_of_le (le : #β ≤ #α) : #{f : α → β | Surjective f} = #(α → β) :=
  mk_surjective_eq_arrow_of_lift_le (lift_le.mpr le)

Cardinality of Surjective Functions Equals Cardinality of All Functions under Cardinality Condition

Informal description

For any types $\alpha$ and $\beta$, if the cardinality of $\beta$ is less than or equal to the cardinality of $\alpha$, then the cardinality of the set of surjective functions from $\alpha$ to $\beta$ equals the cardinality of the set of all functions from $\alpha$ to $\beta$. In symbols: \[ \#\{f : \alpha \to \beta \mid f \text{ is surjective}\} = \#(\alpha \to \beta) \]

Cardinal.mk_list_eq_mk theorem

(α : Type u) [Infinite α] : #(List α) = #α

Full source

@[simp]
theorem mk_list_eq_mk (α : Type u) [Infinite α] : #(List α) = #α :=
  have H1 : ℵ₀ ≤ #α := aleph0_le_mk α
  Eq.symm <|
    le_antisymm ((le_def _ _).2 ⟨⟨fun a => [a], fun _ => by simp⟩⟩) <|
      calc
        #(List α) = sum fun n : ℕ => #α ^ (n : CardinalCardinal.{u}) := mk_list_eq_sum_pow α
        _ ≤ sum fun _ : ℕ => #α := sum_le_sum _ _ fun n => pow_le H1 <| nat_lt_aleph0 n
        _ = #α := by simp [H1]

Cardinality of Lists over Infinite Types: $\#(\text{List}(\alpha)) = \#\alpha$

Informal description

For any infinite type $\alpha$, the cardinality of the set of lists over $\alpha$ equals the cardinality of $\alpha$ itself, i.e., $\#(\text{List}(\alpha)) = \#\alpha$.

Cardinal.mk_list_eq_aleph0 theorem

(α : Type u) [Countable α] [Nonempty α] : #(List α) = ℵ₀

Full source

theorem mk_list_eq_aleph0 (α : Type u) [Countable α] [Nonempty α] : #(List α) = ℵ₀ :=
  mk_le_aleph0.antisymm (aleph0_le_mk _)

Cardinality of Lists over Countable Types Equals Aleph-null

Informal description

For any nonempty countable type $\alpha$, the cardinality of the set of lists over $\alpha$ is equal to $\aleph_0$, i.e., $\#(\text{List } \alpha) = \aleph_0$.

Cardinal.mk_list_eq_max_mk_aleph0 theorem

(α : Type u) [Nonempty α] : #(List α) = max #α ℵ₀

Full source

theorem mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] : #(List α) = max #α ℵ₀ := by
  cases finite_or_infinite α
  · rw [mk_list_eq_aleph0, eq_comm, max_eq_right]
    exact mk_le_aleph0
  · rw [mk_list_eq_mk, eq_comm, max_eq_left]
    exact aleph0_le_mk α

Cardinality of Lists: $\#(\text{List}(\alpha)) = \max(\#\alpha, \aleph_0)$

Informal description

For any nonempty type $\alpha$, the cardinality of the set of lists over $\alpha$ is equal to the maximum of the cardinality of $\alpha$ and $\aleph_0$, i.e., $\#(\text{List}(\alpha)) = \max(\#\alpha, \aleph_0)$.

Cardinal.mk_list_le_max theorem

(α : Type u) : #(List α) ≤ max ℵ₀ #α

Full source

theorem mk_list_le_max (α : Type u) : #(List α) ≤ max ℵ₀ #α := by
  cases finite_or_infinite α
  · exact mk_le_aleph0.trans (le_max_left _ _)
  · rw [mk_list_eq_mk]
    apply le_max_right

Cardinality of Lists Bounded by Maximum of Aleph-null and Type Cardinality

Informal description

For any type $\alpha$, the cardinality of the set of lists over $\alpha$ is bounded above by the maximum of $\aleph_0$ and the cardinality of $\alpha$, i.e., $\#(\text{List}(\alpha)) \leq \max(\aleph_0, \#\alpha)$.

Cardinal.mk_finset_of_infinite theorem

(α : Type u) [Infinite α] : #(Finset α) = #α

Full source

@[simp]
theorem mk_finset_of_infinite (α : Type u) [Infinite α] : #(Finset α) = #α := by
  classical
  exact Eq.symm <|
    le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
      calc
        #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
        _ = #α := mk_list_eq_mk α

Cardinality of Finite Subsets of an Infinite Type: $\#(\text{Finset}(\alpha)) = \#\alpha$

Informal description

For any infinite type $\alpha$, the cardinality of the set of finite subsets of $\alpha$ is equal to the cardinality of $\alpha$ itself, i.e., $\#(\text{Finset}(\alpha)) = \#\alpha$.

Cardinal.mk_bounded_set_le_of_infinite theorem

(α : Type u) [Infinite α] (c : Cardinal) : #{ t : Set α // #t ≤ c } ≤ #α ^ c

Full source

theorem mk_bounded_set_le_of_infinite (α : Type u) [Infinite α] (c : Cardinal) :
    #{ t : Set α // #t ≤ c } ≤ #α ^ c := by
  refine le_trans ?_ (by rw [← add_one_eq (aleph0_le_mk α)])
  induction' c using Cardinal.inductionOn with β
  fapply mk_le_of_surjective
  · intro f
    use Sum.inl ⁻¹' range f
    refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_
    apply mk_range_le
  rintro ⟨s, ⟨g⟩⟩
  classical
  use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)
  apply Subtype.eq; ext x
  constructor
  · rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h
  · intro h
    have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
    use g ⟨x, h⟩
    dsimp only
    rw [dif_pos this]
    congr
    suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
    apply g.2
    exact Classical.choose_spec this

Cardinality Bound for Bounded Subsets of an Infinite Type: $\#\{ t \subseteq \alpha \mid \#t \leq c \} \leq \#\alpha^c$

Informal description

For any infinite type $\alpha$ and any cardinal number $c$, the cardinality of the set of all subsets $t \subseteq \alpha$ with $\#t \leq c$ is at most $\#\alpha^c$.

Cardinal.mk_bounded_set_le theorem

(α : Type u) (c : Cardinal) : #{ t : Set α // #t ≤ c } ≤ max #α ℵ₀ ^ c

Full source

theorem mk_bounded_set_le (α : Type u) (c : Cardinal) :
    #{ t : Set α // #t ≤ c } ≤ max #α ℵ₀ ^ c := by
  trans #{ t : Set ((ULift.{u} ℕ) ⊕ α) // #t ≤ c }
  · refine ⟨Embedding.subtypeMap ?_ ?_⟩
    · apply Embedding.image
      use Sum.inr
      apply Sum.inr.inj
    intro s hs
    exact mk_image_le.trans hs
  apply (mk_bounded_set_le_of_infinite ((ULift.{u} ℕ) ⊕ α) c).trans
  rw [max_comm, ← add_eq_max] <;> rfl

Cardinality Bound for Bounded Subsets: $\#\{ t \subseteq \alpha \mid \#t \leq c \} \leq (\max(\#\alpha, \aleph_0))^c$

Informal description

For any type $\alpha$ and any cardinal number $c$, the cardinality of the set of all subsets $t \subseteq \alpha$ with $\#t \leq c$ is at most $(\max(\#\alpha, \aleph_0))^c$.

Cardinal.mk_bounded_subset_le theorem

{α : Type u} (s : Set α) (c : Cardinal.{u}) : #{ t : Set α // t ⊆ s ∧ #t ≤ c } ≤ max #s ℵ₀ ^ c

Full source

theorem mk_bounded_subset_le {α : Type u} (s : Set α) (c : CardinalCardinal.{u}) :
    #{ t : Set α // t ⊆ s ∧ #t ≤ c } ≤ max #s ℵ₀ ^ c := by
  refine le_trans ?_ (mk_bounded_set_le s c)
  refine ⟨Embedding.codRestrict _ ?_ ?_⟩
  · use fun t => (↑) ⁻¹' t.1
    rintro ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h
    apply Subtype.eq
    dsimp only at h ⊢
    refine (preimage_eq_preimage' ?_ ?_).1 h <;> rw [Subtype.range_coe] <;> assumption
  rintro ⟨t, _, h2t⟩; exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t

Cardinality Bound for Bounded Subsets: $\#\{ t \subseteq s \mid \#t \leq c \} \leq (\max(\#s, \aleph_0))^c$

Informal description

For any type $\alpha$, a subset $s \subseteq \alpha$, and a cardinal number $c$, the cardinality of the set of all subsets $t \subseteq \alpha$ such that $t \subseteq s$ and $\#t \leq c$ is at most $(\max(\#s, \aleph_0))^c$.

Cardinal.mk_compl_of_infinite theorem

{α : Type*} [Infinite α] (s : Set α) (h2 : #s < #α) : #(sᶜ : Set α) = #α

Full source

theorem mk_compl_of_infinite {α : Type*} [Infinite α] (s : Set α) (h2 : #s < #α) :
    #(sᶜ : Set α) = #α := by
  refine eq_of_add_eq_of_aleph0_le ?_ h2 (aleph0_le_mk α)
  exact mk_sum_compl s

Cardinality of Complement Equals Cardinality of Infinite Type for Small Subsets

Informal description

For an infinite type $\alpha$ and a subset $s \subseteq \alpha$ with cardinality strictly less than that of $\alpha$, the complement $s^c$ has the same cardinality as $\alpha$, i.e., $\#(s^c) = \#\alpha$.

Cardinal.mk_compl_finset_of_infinite theorem

{α : Type*} [Infinite α] (s : Finset α) : #((↑s)ᶜ : Set α) = #α

Full source

theorem mk_compl_finset_of_infinite {α : Type*} [Infinite α] (s : Finset α) :
    #((↑s)ᶜ : Set α) = #α := by
  apply mk_compl_of_infinite
  exact (finset_card_lt_aleph0 s).trans_le (aleph0_le_mk α)

Cardinality of Complement of Finite Set in Infinite Type Equals Cardinality of Type

Informal description

For an infinite type $\alpha$ and any finite subset $s \subseteq \alpha$ (represented as a `Finset`), the complement of $s$ in $\alpha$ has the same cardinality as $\alpha$, i.e., $\#(s^c) = \#\alpha$.

Cardinal.mk_compl_eq_mk_compl_infinite theorem

{α : Type*} [Infinite α] {s t : Set α} (hs : #s < #α) (ht : #t < #α) : #(sᶜ : Set α) = #(tᶜ : Set α)

Full source

theorem mk_compl_eq_mk_compl_infinite {α : Type*} [Infinite α] {s t : Set α} (hs : #s < #α)
    (ht : #t < #α) : #(sᶜ : Set α) = #(tᶜ : Set α) := by
  rw [mk_compl_of_infinite s hs, mk_compl_of_infinite t ht]

Equal Cardinality of Complements for Small Subsets of Infinite Types

Informal description

For an infinite type $\alpha$ and subsets $s, t \subseteq \alpha$ with cardinalities strictly less than that of $\alpha$, the complements of $s$ and $t$ have the same cardinality, i.e., $\#(s^c) = \#(t^c)$.

Cardinal.mk_compl_eq_mk_compl_finite_lift theorem

 {α : Type u} {β : Type v} [Finite α] {s : Set α} {t : Set β} (h1 : (lift.{max v w, u} #α) = (lift.{max u w, v} #β))
  (h2 : lift.{max v w, u} #s = lift.{max u w, v} #t) : lift.{max v w} #(sᶜ : Set α) = lift.{max u w} #(tᶜ : Set β)

Full source

theorem mk_compl_eq_mk_compl_finite_lift {α : Type u} {β : Type v} [Finite α] {s : Set α}
    {t : Set β} (h1 : (lift.{max v w, u} #α) = (lift.{max u w, v} #β))
    (h2 : lift.{max v w, u} #s = lift.{max u w, v} #t) :
    lift.{max v w} #(sᶜ : Set α) = lift.{max u w} #(tᶜ : Set β) := by
  cases nonempty_fintype α
  rcases lift_mk_eq.{u, v, w}.1 h1 with ⟨e⟩; letI : Fintype β := Fintype.ofEquiv α e
  replace h1 : Fintype.card α = Fintype.card β := (Fintype.ofEquiv_card _).symm
  classical
    lift s to Finset α using s.toFinite
    lift t to Finset β using t.toFinite
    simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
    simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl,
      lift_natCast, Nat.cast_inj, h1, h2]

Equality of Lifted Cardinalities for Complements of Finite Sets

Informal description

Let $\alpha$ and $\beta$ be types in universes $u$ and $v$ respectively, with $\alpha$ finite. For sets $s \subseteq \alpha$ and $t \subseteq \beta$, if the lifted cardinalities of $\alpha$ and $\beta$ are equal (i.e., $\text{lift}_{\max(v,w)} \#\alpha = \text{lift}_{\max(u,w)} \#\beta$) and the lifted cardinalities of $s$ and $t$ are equal (i.e., $\text{lift}_{\max(v,w)} \#s = \text{lift}_{\max(u,w)} \#t$), then the lifted cardinalities of their complements are also equal (i.e., $\text{lift}_{\max(v,w)} \#(s^c) = \text{lift}_{\max(u,w)} \#(t^c)$).

Cardinal.mk_compl_eq_mk_compl_finite theorem

 {α β : Type u} [Finite α] {s : Set α} {t : Set β} (h1 : #α = #β) (h : #s = #t) : #(sᶜ : Set α) = #(tᶜ : Set β)

Full source

theorem mk_compl_eq_mk_compl_finite {α β : Type u} [Finite α] {s : Set α} {t : Set β}
    (h1 : #α = #β) (h : #s = #t) : #(sᶜ : Set α) = #(tᶜ : Set β) := by
  rw [← lift_inj.{u, u}]
  apply mk_compl_eq_mk_compl_finite_lift.{u, u, u}
  <;> rwa [lift_inj]

Equal Cardinality of Complements for Finite Sets with Equal Cardinalities

Informal description

Let $\alpha$ and $\beta$ be finite types with the same cardinality (i.e., $\#\alpha = \#\beta$). For any subsets $s \subseteq \alpha$ and $t \subseteq \beta$ with $\#s = \#t$, the complements of $s$ and $t$ also have the same cardinality (i.e., $\#(s^c) = \#(t^c)$).

Cardinal.mk_compl_eq_mk_compl_finite_same theorem

{α : Type u} [Finite α] {s t : Set α} (h : #s = #t) : #(sᶜ : Set α) = #(tᶜ : Set α)

Full source

theorem mk_compl_eq_mk_compl_finite_same {α : Type u} [Finite α] {s t : Set α} (h : #s = #t) :
    #(sᶜ : Set α) = #(tᶜ : Set α) :=
  mk_compl_eq_mk_compl_finite.{u} rfl h

Equal Cardinality of Complements for Finite Sets with Equal Cardinalities in Same Type

Informal description

For a finite type $\alpha$ and any two subsets $s, t \subseteq \alpha$ with the same cardinality (i.e., $\#s = \#t$), the complements of $s$ and $t$ also have the same cardinality (i.e., $\#(s^c) = \#(t^c)$).

Cardinal.extend_function theorem

 {α β : Type*} {s : Set α} (f : s ↪ β) (h : Nonempty ((sᶜ : Set α) ≃ ((range f)ᶜ : Set β))) :
  ∃ g : α ≃ β, ∀ x : s, g x = f x

Full source

theorem extend_function {α β : Type*} {s : Set α} (f : s ↪ β)
    (h : Nonempty ((sᶜ : Set α) ≃ ((range f)ᶜ : Set β))) : ∃ g : α ≃ β, ∀ x : s, g x = f x := by
  classical
  have := h; obtain ⟨g⟩ := this
  let h : α ≃ β :=
    (Set.sumCompl (s : Set α)).symm.trans
      ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
  refine ⟨h, ?_⟩; rintro ⟨x, hx⟩; simp [h, Set.sumCompl_symm_apply_of_mem, hx]

Extension of Injective Function to Equivalence via Complement Equivalence

Informal description

Let $\alpha$ and $\beta$ be types, and let $s$ be a subset of $\alpha$. Given an injective function $f : s \hookrightarrow \beta$ and a nonempty equivalence between the complement of $s$ in $\alpha$ and the complement of the range of $f$ in $\beta$, there exists an equivalence $g : \alpha \simeq \beta$ such that for every $x \in s$, $g(x) = f(x)$.

Cardinal.extend_function_finite theorem

 {α : Type u} {β : Type v} [Finite α] {s : Set α} (f : s ↪ β) (h : Nonempty (α ≃ β)) : ∃ g : α ≃ β, ∀ x : s, g x = f x

Full source

theorem extend_function_finite {α : Type u} {β : Type v} [Finite α] {s : Set α} (f : s ↪ β)
    (h : Nonempty (α ≃ β)) : ∃ g : α ≃ β, ∀ x : s, g x = f x := by
  apply extend_function.{u, v} f
  obtain ⟨g⟩ := id h
  rw [← lift_mk_eq.{u, v, max u v}] at h
  rw [← lift_mk_eq.{u, v, max u v}, mk_compl_eq_mk_compl_finite_lift.{u, v, max u v} h]
  rw [mk_range_eq_lift.{u, v, max u v}]; exact f.2

Extension of Injective Function to Equivalence for Finite Types

Informal description

Let $\alpha$ and $\beta$ be types with $\alpha$ finite, and let $s$ be a subset of $\alpha$. Given an injective function $f \colon s \hookrightarrow \beta$ and a nonempty equivalence between $\alpha$ and $\beta$, there exists an equivalence $g \colon \alpha \simeq \beta$ such that for every $x \in s$, $g(x) = f(x)$.

Cardinal.extend_function_of_lt theorem

 {α β : Type*} {s : Set α} (f : s ↪ β) (hs : #s < #α) (h : Nonempty (α ≃ β)) : ∃ g : α ≃ β, ∀ x : s, g x = f x

Full source

theorem extend_function_of_lt {α β : Type*} {s : Set α} (f : s ↪ β) (hs : #s < #α)
    (h : Nonempty (α ≃ β)) : ∃ g : α ≃ β, ∀ x : s, g x = f x := by
  cases fintypeOrInfinite α
  · exact extend_function_finite f h
  · apply extend_function f
    obtain ⟨g⟩ := id h
    haveI := Infinite.of_injective _ g.injective
    rw [← lift_mk_eq'] at h ⊢
    rwa [mk_compl_of_infinite s hs, mk_compl_of_infinite]
    rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]

Extension of Injective Function to Equivalence for Small Subsets

Informal description

Let $\alpha$ and $\beta$ be types, and let $s$ be a subset of $\alpha$ with cardinality strictly less than that of $\alpha$ (i.e., $\#s < \#\alpha$). Given an injective function $f \colon s \hookrightarrow \beta$ and a nonempty equivalence between $\alpha$ and $\beta$, there exists an equivalence $g \colon \alpha \simeq \beta$ such that for every $x \in s$, $g(x) = f(x)$.

Mathlib.SetTheory.Cardinal.Arithmetic

Main statements

Tags