ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ ∀ (x : ι), x ∈ Set.Ioi i → i ≤ x
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ i ≤ succFn i
rw [le_isGLB_iff (succFn_spec i), mem_lowerBounds]
no goals
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ ∀ (x : ι), x ∈ Set.Ioi i → i ≤ x
exact fun x hx ↦ le_of_lt hx