le_mk_iff_exists_set — Mathlib

English

For a cardinal c and a type α, we have c ≤ |α| if and only if there exists a subset p of α with |p| = c.

Русский

Для кардинала c и типа α верно: c ≤ |α| тогда и только тогда существует подмножество p ⊆ α такое, что |p| = c.

LaTeX

$$$$ c \\le |\\\\alpha| \\iff \\exists p \\subseteq \\\\alpha, |p| = c. $$$$

Lean4

theorem le_mk_iff_exists_set {c : Cardinal} {α : Type u} : c ≤ #α ↔ ∃ p : Set α, #p = c :=
  ⟨inductionOn c fun _ ⟨⟨f, hf⟩⟩ => ⟨Set.range f, (Equiv.ofInjective f hf).cardinal_eq.symm⟩, fun ⟨_, e⟩ =>
    e ▸ ⟨⟨Subtype.val, fun _ _ => Subtype.eq⟩⟩⟩

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