case intro
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
⊢ ∃ᶠ (x : α) in 𝓝[Iic a] a, x ∈ s
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
hs : Set.Nonempty s
⊢ ∃ᶠ (x : α) in 𝓝[Iic a] a, x ∈ s
rcases hs with ⟨a', ha'⟩
case intro
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[Iic a] a, ¬(fun x => x ∈ s) x
⊢ False
case intro
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
⊢ ∃ᶠ (x : α) in 𝓝[Iic a] a, x ∈ s
intro h
case intro.inl
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
s : Set α
a' : α
ha' : a' ∈ s
ha : IsLUB s a'
h : ∀ᶠ (x : α) in 𝓝[Iic a'] a', ¬(fun x => x ∈ s) x
⊢ False

case intro.inr
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[Iic a] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
⊢ False
case intro
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[Iic a] a, ¬(fun x => x ∈ s) x
⊢ False
rcases(ha.1 ha').eq_or_lt with (rfl | ha'a)
no goals
case intro.inl
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
s : Set α
a' : α
ha' : a' ∈ s
ha : IsLUB s a'
h : ∀ᶠ (x : α) in 𝓝[Iic a'] a', ¬(fun x => x ∈ s) x
⊢ False
exact h.self_of_nhdsWithin le_rfl ha'
case intro.inr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[Iic a] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x => ¬(fun x => x ∈ s) x) x}
⊢ False
case intro.inr
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[Iic a] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
⊢ False
rcases (mem_nhdsWithin_Iic_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩
case intro.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[Iic a] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x => ¬(fun x => x ∈ s) x) x}
b' : α
hb's : b' ∈ s
hb' : b < b' ∧ b' ≤ a
⊢ False
case intro.inr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[Iic a] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x => ¬(fun x => x ∈ s) x) x}
⊢ False
rcases ha.exists_between hba with ⟨b', hb's, hb'⟩
no goals
case intro.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[Iic a] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x => ¬(fun x => x ∈ s) x) x}
b' : α
hb's : b' ∈ s
hb' : b < b' ∧ b' ≤ a
⊢ False
exact hb hb' hb's