English
There exists an index i with injections from β(i) into all β(j).
Русский
Существует индекс i, для которого β(i) инъективно вкладывается во все β(j).
LaTeX
$$$\exists i, \forall j, β(i) \hookrightarrow β(j)$$$
Lean4
theorem cardinalMk_closure_le_max : #(closure s) ≤ max #s ℵ₀ :=
(Cardinal.mk_le_of_surjective <| surjective_ofWType s).trans <|
by
convert WType.cardinalMk_le_max_aleph0_of_finite' using 1
· rw [lift_uzero, mk_sum, lift_uzero]
have : lift.{u, 0} #(Fin 6) < ℵ₀ := lift_lt_aleph0.mpr (lt_aleph0_of_finite _)
obtain h | h := lt_or_ge #s ℵ₀
· rw [max_eq_right h.le, max_eq_right]
exact (add_lt_aleph0 this h).le
· rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]
rintro (n | _)
· fin_cases n <;> (dsimp only [id_eq]; infer_instance)
infer_instance
