α : Type ?u.353871
β : Type ?u.353874
γ : Type ?u.353877
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ sup (familyOfBFamily o f) = lsub (familyOfBFamily o f) ∨ succ (sup (familyOfBFamily o f)) = lsub (familyOfBFamily o f)
α : Type ?u.353871
β : Type ?u.353874
γ : Type ?u.353877
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ bsup o f = blsub o f ∨ succ (bsup o f) = blsub o f
rw [← sup_eq_bsup, ← lsub_eq_blsub]
no goals
α : Type ?u.353871
β : Type ?u.353874
γ : Type ?u.353877
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ sup (familyOfBFamily o f) = lsub (familyOfBFamily o f) ∨ succ (sup (familyOfBFamily o f)) = lsub (familyOfBFamily o f)
exact sup_eq_lsub_or_sup_succ_eq_lsub _