s : Set Ordinal
a : Ordinal
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s) → IsClosed s
s : Set Ordinal
a : Ordinal
⊢ IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s
use fun hs ι hι f hf => (mem_closed_iff_sup hs).2 ⟨ι, hι, f, hf, rfl⟩
s : Set Ordinal
a : Ordinal
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s) → closure s ⊆ s
s : Set Ordinal
a : Ordinal
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s) → IsClosed s
rw [← closure_subset_iff_isClosed]
s : Set Ordinal
a : Ordinal
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s
x : Ordinal
hx : x ∈ closure s
⊢ x ∈ s
s : Set Ordinal
a : Ordinal
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s) → closure s ⊆ s
intro h x hx
case intro.intro.intro.intro
s : Set Ordinal
a : Ordinal
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal
hf : ∀ (i : ι), f i ∈ s
hx : sup f ∈ closure s
⊢ sup f ∈ s
s : Set Ordinal
a : Ordinal
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s
x : Ordinal
hx : x ∈ closure s
⊢ x ∈ s
rcases mem_closure_iff_sup.1 hx with ⟨ι, hι, f, hf, rfl⟩
no goals
case intro.intro.intro.intro
s : Set Ordinal
a : Ordinal
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal
hf : ∀ (i : ι), f i ∈ s
hx : sup f ∈ closure s
⊢ sup f ∈ s
exact h hι f hf