α : Type ?u.357763
β : Type ?u.357766
γ : Type ?u.357769
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ IsEmpty (Quotient.out o).α ↔ o = 0
α : Type ?u.357763
β : Type ?u.357766
γ : Type ?u.357769
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ blsub o f = 0 ↔ o = 0
rw [← lsub_eq_blsub, lsub_eq_zero_iff]
no goals
α : Type ?u.357763
β : Type ?u.357766
γ : Type ?u.357769
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ IsEmpty (Quotient.out o).α ↔ o = 0
exact out_empty_iff_eq_zero