α : Type ?u.326038
β : Type ?u.326041
γ : Type ?u.326044
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
i : ι
⊢ f i < lsub f
α : Type ?u.326038
β : Type ?u.326041
γ : Type ?u.326044
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
i : ι
⊢ f i < sup f
rw [h]
no goals
α : Type ?u.326038
β : Type ?u.326041
γ : Type ?u.326044
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
i : ι
⊢ f i < lsub f
apply lt_lsub