α : Type ?u.356089
β : Type ?u.356092
γ : Type ?u.356095
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ sup (familyOfBFamily o f) = lsub (familyOfBFamily o f) ↔
    ∀ (a : Ordinal), a < lsub (familyOfBFamily o f) → succ a < lsub (familyOfBFamily o f)
α : Type ?u.356089
β : Type ?u.356092
γ : Type ?u.356095
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ bsup o f = blsub o f ↔ ∀ (a : Ordinal), a < blsub o f → succ a < blsub o f
rw [← sup_eq_bsup, ← lsub_eq_blsub]
no goals
α : Type ?u.356089
β : Type ?u.356092
γ : Type ?u.356095
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ sup (familyOfBFamily o f) = lsub (familyOfBFamily o f) ↔
    ∀ (a : Ordinal), a < lsub (familyOfBFamily o f) → succ a < lsub (familyOfBFamily o f)
apply sup_eq_lsub_iff_succ