small_Iic — Mathlib

English

For every cardinal a, the set of cardinals not exceeding a is small.

Русский

Для каждого кардинала a множество кардиналов, не превосходящих a, мало.

LaTeX

$$Iic(a) is small$$

Lean4

instance small_Iic (a : Cardinal.{u}) : Small.{u} (Iic a) :=
  by
  rw [← mk_out a]
  apply @small_of_surjective (Set a.out) (Iic #a.out) _ fun x => ⟨#x, mk_set_le x⟩
  rintro ⟨x, hx⟩
  simpa using le_mk_iff_exists_set.1 hx

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