Limit elements in Set.Ici

If J is a linearly ordered type, j : J, and m : Set.Ici j is successor limit, then ↑m : J is also successor limit.

theorem Set.Ici.isSuccLimit_coe {J : Type u} [LinearOrder J] {j : J} (m : ↑(Ici j)) (hm : Order.IsSuccLimit m) : Order.IsSuccLimit ↑m