isSuccLimit — Mathlib

English

There is a correspondence between accumulation points below o and accumulation points of the restricted set inside the initial segment.

Русский

Существует соответствие между точками накопления ниже o и точками накопления внутри начального отрезка.

LaTeX

$$accPt_subtype {p o : Ordinal} (S : Set Ordinal) (hpo : p < o) : AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))$$

Lean4

theorem isSuccLimit {o : Ordinal} {S : Set Ordinal} (h : o.IsAcc S) : IsSuccLimit o :=
  by
  rw [isAcc_iff] at h
  rw [isSuccLimit_iff]
  refine ⟨h.1, isSuccPrelimit_of_succ_ne fun x hx ↦ ?_⟩
  rcases h.2 x (lt_of_lt_of_le (lt_succ x) hx.le) with ⟨p, hp⟩
  exact (hx.symm ▸ (succ_le_iff.mpr hp.2.1)).not_gt hp.2.2

Похожие утверждения