English
For any o and S, o is an accumulation point of S if and only if o ≠ 0 and every p < o yields that S ∩ Ioo(p,o) is nonempty.
Русский
Для любых o и S, o является точкой накопления S тогда и только тогда, когда o ≠ 0 и для каждого p < o множество S ∩ Ioo(p,o) непусто.
LaTeX
$$IsAcc o S ↔ (o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty).$$
Lean4
theorem isAcc_iff (o : Ordinal) (S : Set Ordinal) : o.IsAcc S ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty :=
by
dsimp [IsAcc]
constructor
· rw [accPt_iff_nhds]
intro h
constructor
· rintro rfl
obtain ⟨x, hx⟩ := h (Iio 1) (Iio_mem_nhds zero_lt_one)
exact hx.2 <| lt_one_iff_zero.mp hx.1.1
· intro p plt
obtain ⟨x, hx⟩ := h (Ioo p (o + 1)) <| Ioo_mem_nhds plt (lt_succ o)
use x
refine ⟨hx.1.2, ⟨hx.1.1.1, lt_of_le_of_ne ?_ hx.2⟩⟩
have := hx.1.1.2
rwa [← succ_eq_add_one, lt_succ_iff] at this
· rw [accPt_iff_nhds]
intro h u umem
obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds umem ⟨0, Ordinal.pos_iff_ne_zero.mpr h.1⟩
obtain ⟨x, hx⟩ := h.2 l hl.1
use x
exact ⟨⟨hl.2 ⟨hx.2.1, hx.2.2.le⟩, hx.1⟩, hx.2.2.ne⟩
