nonempty_embedding_to_cardinal — Mathlib

English

There exists an embedding from any type α into Cardinal.

Русский

Существует вложение (в виде инъекции) из любого типа α в множество кардиналов.

LaTeX

$$$\\exists (e : α \\hookrightarrow \\mathrm{Cardinal})$$$

Lean4

theorem nonempty_embedding_to_cardinal : Nonempty (α ↪ Cardinal.{u}) :=
  (Embedding.total _ _).resolve_left fun ⟨⟨f, hf⟩⟩ =>
    let g : α → Cardinal.{u} := invFun f
    let ⟨x, (hx : g x = 2 ^ sum g)⟩ := invFun_surjective hf (2 ^ sum g)
    have : g x ≤ sum g := le_sum.{u, u} g x
    not_le_of_gt (by rw [hx]; exact cantor _) this

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