α : Type ?u.144886
r : α → α → Prop
c : Cardinal
H : IsRegular c
⊢ card 0 < c
α : Type ?u.144886
r : α → α → Prop
c : Cardinal
H : IsRegular c
⊢ 0 < ord c
rw [Cardinal.lt_ord]
no goals
α : Type ?u.144886
r : α → α → Prop
c : Cardinal
H : IsRegular c
⊢ card 0 < c
exact H.pos