mul_eq_self — Mathlib

English

If c is an infinite cardinal, then c × c = c.

Русский

Если c бесконечная кардинальная величина, то c × c = c.

LaTeX

$$$c \cdot c = c$$$

Lean4

/-- 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
  rcases ord_eq α with ⟨r, wo, e⟩
  classical
  letI := linearOrderOfSTO r
  haveI : IsWellOrder α (· < ·) := wo
  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
  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} ⊆ 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_ge (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 (isSuccLimit_ord ol).succ_lt
    rw [e]
    apply typein_lt_type

Похожие утверждения