α : Type ?u.21687
r : α → α → Prop
o : Ordinal
⊢ ∃ ι f, lsub f = o ∧ (#ι) = sInf {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
α : Type ?u.21687
r : α → α → Prop
o : Ordinal
⊢ ∃ ι f, lsub f = o ∧ (#ι) = cof o
rw [cof_eq_sInf_lsub]
no goals
α : Type ?u.21687
r : α → α → Prop
o : Ordinal
⊢ ∃ ι f, lsub f = o ∧ (#ι) = sInf {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
exact csInf_mem (cof_lsub_def_nonempty o)