mk_bounded_set_le — Mathlib

English

For any α and any c, the family of subsets t of α with |t| ≤ c has cardinality at most max(|α|, ℵ0)^c.

Русский

Для любых α и c множество подмножеств t ⊆ α с ≤ c элементами имеет кардинальность не более max(|α|, ℵ0)^c.

LaTeX

$$$\\#\\{ t \\subseteq \\alpha \\;|\\; \\#t \\le c \\} \\le \\max\\{\\#\\alpha, \\aleph_{0}\\}^{\\,c}$$$

Lean4

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

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