ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : IsGLB (Set.Ioi i) (succFn i)
⊢ succFn i ≤ j
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
⊢ succFn i ≤ j
have h := succFn_spec i
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : (∀ (x : ι), x ∈ Set.Ioi i → succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : IsGLB (Set.Ioi i) (succFn i)
⊢ succFn i ≤ j
rw [IsGLB, IsGreatest, mem_lowerBounds] at h
no goals
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : (∀ (x : ι), x ∈ Set.Ioi i → succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j
exact h.1 j hij