s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
⊢ IsLimit a
s : Set Ordinal
a : Ordinal
ha : a ∈ frontier s
⊢ IsLimit a
simp only [frontier_eq_closure_inter_closure, Set.mem_inter_iff, mem_closure_iff] at ha
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : ¬IsLimit a
⊢ False
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
⊢ IsLimit a
by_contra h
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
⊢ False
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : ¬IsLimit a
⊢ False
rw [← isOpen_singleton_iff] at h
case intro.intro
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal
hb : b ∈ {a}
hb' : b ∈ s
⊢ False
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
⊢ False
rcases ha.1 _ h rfl with ⟨b, hb, hb'⟩
case intro.intro.intro.intro
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal
hb : b ∈ {a}
hb' : b ∈ s
c : Ordinal
hc : c ∈ {a}
hc' : c ∈ sᶜ
⊢ False
case intro.intro
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal
hb : b ∈ {a}
hb' : b ∈ s
⊢ False
rcases ha.2 _ h rfl with ⟨c, hc, hc'⟩
case intro.intro.intro.intro
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal
hb : b = a
hb' : b ∈ s
c : Ordinal
hc : c = a
hc' : c ∈ sᶜ
⊢ False
case intro.intro.intro.intro
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal
hb : b ∈ {a}
hb' : b ∈ s
c : Ordinal
hc : c ∈ {a}
hc' : c ∈ sᶜ
⊢ False
rw [Set.mem_singleton_iff] at *
case intro.intro.intro.intro
s : Set Ordinal
b : Ordinal
hb' : b ∈ s
c : Ordinal
hc' : c ∈ sᶜ
ha :
  (∀ (o : Set Ordinal), IsOpen o → b ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → b ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {b}
hc : c = b
⊢ False
case intro.intro.intro.intro
s : Set Ordinal
a : Ordinal
ha :
  (∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → a ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {a}
b : Ordinal
hb : b = a
hb' : b ∈ s
c : Ordinal
hc : c = a
hc' : c ∈ sᶜ
⊢ False
subst hb
case intro.intro.intro.intro
s : Set Ordinal
c : Ordinal
hc' : c ∈ sᶜ
hb' : c ∈ s
ha :
  (∀ (o : Set Ordinal), IsOpen o → c ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → c ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {c}
⊢ False
case intro.intro.intro.intro
s : Set Ordinal
b : Ordinal
hb' : b ∈ s
c : Ordinal
hc' : c ∈ sᶜ
ha :
  (∀ (o : Set Ordinal), IsOpen o → b ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → b ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {b}
hc : c = b
⊢ False
subst hc
no goals
case intro.intro.intro.intro
s : Set Ordinal
c : Ordinal
hc' : c ∈ sᶜ
hb' : c ∈ s
ha :
  (∀ (o : Set Ordinal), IsOpen o → c ∈ o → Set.Nonempty (o ∩ s)) ∧
    ∀ (o : Set Ordinal), IsOpen o → c ∈ o → Set.Nonempty (o ∩ sᶜ)
h : IsOpen {c}
⊢ False
exact hc' hb'