English
A set is closed below o iff every p < o that is an accumulation point of S is in S.
Русский
Множество замкнуто ниже o тогда и только тогда, когда для каждого p < o, являющегося точкой накопления S, верно p ∈ S.
LaTeX
$$isClosedBelow_iff {S : Set Ordinal} {o : Ordinal} : IsClosedBelow S o ↔ ∀ p < o, IsAcc p S → p ∈ S$$
Lean4
theorem isClosedBelow_iff {S : Set Ordinal} {o : Ordinal} : IsClosedBelow S o ↔ ∀ p < o, IsAcc p S → p ∈ S :=
by
dsimp [IsClosedBelow]
constructor
· intro h p plto hp
have : AccPt ⟨p, plto⟩ (𝓟 (Iio o ↓∩ S)) := (accPt_subtype _ _).mp hp
rw [isClosed_iff_clusterPt] at h
exact h ⟨p, plto⟩ this.clusterPt
· intro h
rw [isClosed_iff_clusterPt]
intro r hr
match clusterPt_principal.mp hr with
| .inl h => exact h
| .inr h' => exact h r.1 r.2 <| (accPt_subtype _ _).mpr h'
