English
If m ∈ Set.Ici j is a succ-limit in the ambient order, then its projection m.1 is succ-limit in the ambient type as well; succ-limit is preserved under the coercion from the interval to the ambient order.
Русский
Если m ∈ Set.Ici j является пределом поsucc в исходном порядке, то и его проекция m.1 имеет тот же свойство в базовом порядке; предел по succ сохраняется при каноническом отображении.
LaTeX
$$$\\forall m:\\ (Set.Ici\\ j).Elem,\\, \\mathrm{Order.IsSuccLimit}(m) \\Rightarrow \\mathrm{Order.IsSuccLimit}(m.1)$$$
Lean4
theorem isSuccLimit_coe {J : Type u} [LinearOrder J] {j : J} (m : Set.Ici j) (hm : Order.IsSuccLimit m) :
Order.IsSuccLimit m.1 :=
⟨Set.not_isMin_coe _ hm.1, fun b ↦
by
simp only [CovBy, not_lt, not_and, not_forall, not_le]
intro hb
by_cases hb' : j ≤ b
· have := hm.2 ⟨b, hb'⟩
rw [not_covBy_iff (by exact hb)] at this
obtain ⟨⟨x, h₁⟩, h₂, h₃⟩ := this
refine ⟨x, h₂, h₃⟩
· simp only [not_le] at hb'
refine ⟨j, hb', ?_⟩
by_contra!
apply hm.1
rintro ⟨k, hk⟩ _
exact this.trans (by simpa using hk)⟩
