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)
: