English
A reiteration of accPt_subtype identifying the subtype relationship for accumulation points.
Русский
Повторение accPt_subtype с указанием отношения подтипа точек накопления.
LaTeX
$$accPt_subtype {p o : Ordinal} (S : Set Ordinal) (hpo : p < o) : AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))$$
Lean4
theorem accPt_subtype {p o : Ordinal} (S : Set Ordinal) (hpo : p < o) :
AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S)) :=
by
constructor
· intro h
have plim := IsAcc.isSuccLimit h
rw [accPt_iff_nhds] at *
intro u hu
obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds hu ⟨⟨0, plim.bot_lt.trans hpo⟩, plim.bot_lt⟩
obtain ⟨x, hx⟩ := h (Ioo l (p + 1)) (Ioo_mem_nhds hl.1 (lt_add_one _))
use ⟨x, lt_of_le_of_lt (lt_succ_iff.mp hx.1.1.2) hpo⟩
refine ⟨?_, Subtype.coe_ne_coe.mp hx.2⟩
exact ⟨hl.2 ⟨hx.1.1.1, by exact_mod_cast lt_succ_iff.mp hx.1.1.2⟩, hx.1.2⟩
· intro h
rw [accPt_iff_nhds] at *
intro u hu
by_cases ho : p + 1 < o
· have ppos : p ≠ 0 := by
rintro rfl
rw [zero_add] at ho
specialize h (Iio ⟨1, ho⟩) (Iio_mem_nhds (Subtype.mk_lt_mk.mpr zero_lt_one))
obtain ⟨_, h⟩ := h
exact h.2 <| Subtype.mk_eq_mk.mpr (lt_one_iff_zero.mp h.1.1)
have plim : IsSuccLimit p := by
contrapose! h
obtain ⟨q, hq⟩ := ((zero_or_succ_or_isSuccLimit p).resolve_left ppos).resolve_right h
use (Ioo ⟨q, ((hq ▸ lt_succ q).trans hpo)⟩ ⟨p + 1, ho⟩)
constructor
· exact Ioo_mem_nhds (hq ▸ lt_succ q) (lt_succ p)
· intro _ mem
have aux1 := Subtype.mk_lt_mk.mp mem.1.1
have aux2 := Subtype.mk_lt_mk.mp mem.1.2
rw [Subtype.mk_eq_mk]
subst hq
exact ((succ_le_iff.mpr aux1).antisymm (le_of_lt_succ aux2)).symm
obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds hu ⟨0, plim.bot_lt⟩
obtain ⟨x, hx⟩ := h (Ioo ⟨l, hl.1.trans hpo⟩ ⟨p + 1, ho⟩) (Ioo_mem_nhds hl.1 (lt_add_one p))
use x
exact ⟨⟨hl.2 ⟨hx.1.1.1, lt_succ_iff.mp hx.1.1.2⟩, hx.1.2⟩, fun h ↦ hx.2 (SetCoe.ext h)⟩
have hp : o = p + 1 := (le_succ_iff_eq_or_le.mp (le_of_not_gt ho)).resolve_right (not_le_of_gt hpo)
have ppos : p ≠ 0 := by
rintro rfl
obtain ⟨x, hx⟩ := h Set.univ univ_mem
have : ↑x < o := x.2
simp_rw [hp, zero_add, lt_one_iff_zero] at this
exact hx.2 (SetCoe.ext this)
obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds hu ⟨0, Ordinal.pos_iff_ne_zero.mpr ppos⟩
obtain ⟨x, hx⟩ := h (Ioi ⟨l, hl.1.trans hpo⟩) (Ioi_mem_nhds hl.1)
use x
refine ⟨⟨hl.2 ⟨hx.1.1, ?_⟩, hx.1.2⟩, fun h ↦ hx.2 (SetCoe.ext h)⟩
rw [← lt_add_one_iff, ← hp]
exact x.2
