α : Type ?u.326516
β : Type ?u.326519
γ : Type ?u.326522
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u_1
h : IsEmpty ι
f : ι → Ordinal
⊢ ∀ (i : ι), f i < 0
α : Type ?u.326516
β : Type ?u.326519
γ : Type ?u.326522
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u_1
h : IsEmpty ι
f : ι → Ordinal
⊢ lsub f = 0
rw [← Ordinal.le_zero, lsub_le_iff]
no goals
α : Type ?u.326516
β : Type ?u.326519
γ : Type ?u.326522
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u_1
h : IsEmpty ι
f : ι → Ordinal
⊢ ∀ (i : ι), f i < 0
exact h.elim