English
For any cardinal c, c + 1 ≤ succ(c). The successor dominates adding one.
Русский
Для любого кардинала c верно, что c + 1 ≤ succ(c). Преемник доминирует над прибавлением единицы.
LaTeX
$$$c + 1 \\leq \\operatorname{succ}(c)$$$
Lean4
theorem add_one_le_succ (c : Cardinal.{u}) : c + 1 ≤ succ c :=
by
have : Set.Nonempty {c' | c < c'} := exists_gt c
simp_rw [succ_def, le_csInf_iff'' this, mem_setOf]
intro b hlt
rcases b, c with ⟨⟨β⟩, ⟨γ⟩⟩
obtain ⟨f⟩ := le_of_lt hlt
have : ¬Surjective f := fun hn => (not_le_of_gt hlt) (mk_le_of_surjective hn)
simp only [Surjective, not_forall] at this
rcases this with ⟨b, hb⟩
calc
#γ + 1 = #(Option γ) := mk_option.symm
_ ≤ #β := (f.optionElim b hb).cardinal_le
