case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
hb' : Iio b = ∅
⊢ map Subtype.val atTop = 𝓝[Iio b] b

case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ map Subtype.val atTop = 𝓝[Iio b] b
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
⊢ map Subtype.val atTop = 𝓝[Iio b] b
rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
hb' : Iio b = ∅
this : IsEmpty ↑s
⊢ map Subtype.val atTop = 𝓝[Iio b] b
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
hb' : Iio b = ∅
⊢ map Subtype.val atTop = 𝓝[Iio b] b
have : IsEmpty s := ⟨fun x => hb'.subset (hb x.2)⟩
no goals
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
hb' : Iio b = ∅
this : IsEmpty ↑s
⊢ map Subtype.val atTop = 𝓝[Iio b] b
rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ range Subtype.val ∈ 𝓝[Iio b] b
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ map Subtype.val atTop = 𝓝[Iio b] b
rw [← comap_coe_nhdsWithin_Iio_of_Ioo_subset hb fun _ => hs a ha, map_comap_of_mem]
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ s ∈ 𝓝[Iio b] b
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ range Subtype.val ∈ 𝓝[Iio b] b
rw [Subtype.range_val]
no goals
case inr.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ (a' : α), a' < b → ∃ a, a < b ∧ Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ s ∈ 𝓝[Iio b] b
exact (mem_nhdsWithin_Iio_iff_exists_Ioo_subset' ha).2 (hs a ha)