α : Type ?u.147584
r : α → α → Prop
⊢ IsRegular (succ ℵ₀)
α : Type ?u.147584
r : α → α → Prop
⊢ IsRegular (aleph 1)
rw [← succ_aleph0]
no goals
α : Type ?u.147584
r : α → α → Prop
⊢ IsRegular (succ ℵ₀)
exact isRegular_succ le_rfl