α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
⊢ comap Subtype.val (𝓝[Iio b] b) = atTop
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
⊢ comap Subtype.val (𝓝[Iio b] b) = atTop
nontriviality
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
⊢ comap Subtype.val (𝓝[Iio b] b) = atTop
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
⊢ comap Subtype.val (𝓝[Iio b] b) = atTop
haveI : Nonempty s := nontrivial_iff_nonempty.1 ‹_›
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
⊢ comap Subtype.val (𝓝[Iio b] b) = atTop
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hb : s ⊆ Iio b
hs : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
⊢ comap Subtype.val (𝓝[Iio b] b) = atTop
rcases hs (nonempty_subtype.1 ‹_›) with ⟨a, h, hs⟩
case intro.intro.a
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ comap Subtype.val (𝓝[Iio b] b) ↔ u ∈ atTop
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
⊢ comap Subtype.val (𝓝[Iio b] b) = atTop
ext u
case intro.intro.a.mp
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ comap Subtype.val (𝓝[Iio b] b) → u ∈ atTop

case intro.intro.a.mpr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ atTop → u ∈ comap Subtype.val (𝓝[Iio b] b)
case intro.intro.a
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ comap Subtype.val (𝓝[Iio b] b) ↔ u ∈ atTop
constructor
case intro.intro.a.mp.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
⊢ u ∈ atTop
case intro.intro.a.mp
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ comap Subtype.val (𝓝[Iio b] b) → u ∈ atTop
rintro ⟨t, ht, hts⟩
case intro.intro.a.mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
⊢ u ∈ atTop
case intro.intro.a.mp.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
⊢ u ∈ atTop
obtain ⟨x, ⟨hxa : a ≤ x, hxb : x < b⟩, hxt : Ioo x b ⊆ t⟩ :=
  (mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset h).mp ht
case intro.intro.a.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
y : α
hxy : x < y
hyb : y < b
⊢ u ∈ atTop
case intro.intro.a.mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
⊢ u ∈ atTop
obtain ⟨y, hxy, hyb⟩ := exists_between hxb
case intro.intro.a.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
y : α
hxy : x < y
hyb : y < b
⊢ {b_1 | { val := y, property := (_ : y ∈ s) } ≤ b_1} ⊆ u
case intro.intro.a.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
y : α
hxy : x < y
hyb : y < b
⊢ u ∈ atTop
refine' mem_of_superset (mem_atTop ⟨y, hs ⟨hxa.trans_lt hxy, hyb⟩⟩) _
case intro.intro.a.mp.intro.intro.intro.intro.intro.intro.intro.mk
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
y : α
hxy : x < y
hyb : y < b
z : α
hzs : z ∈ s
hyz : y ≤ z
⊢ { val := z, property := hzs } ∈ u
case intro.intro.a.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
y : α
hxy : x < y
hyb : y < b
⊢ {b_1 | { val := y, property := (_ : y ∈ s) } ≤ b_1} ⊆ u
rintro ⟨z, hzs⟩ (hyz : y ≤ z)
no goals
case intro.intro.a.mp.intro.intro.intro.intro.intro.intro.intro.mk
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[Iio b] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
y : α
hxy : x < y
hyb : y < b
z : α
hzs : z ∈ s
hyz : y ≤ z
⊢ { val := z, property := hzs } ∈ u
exact hts (hxt ⟨hxy.trans_le hyz, hb hzs⟩)
case intro.intro.a.mpr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
hu : u ∈ atTop
⊢ u ∈ comap Subtype.val (𝓝[Iio b] b)
case intro.intro.a.mpr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ atTop → u ∈ comap Subtype.val (𝓝[Iio b] b)
intro hu
case intro.intro.a.mpr.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
hu : u ∈ atTop
x : ↑s
hx : ∀ (z : ↑s), x ≤ z → z ∈ u
⊢ u ∈ comap Subtype.val (𝓝[Iio b] b)
case intro.intro.a.mpr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
hu : u ∈ atTop
⊢ u ∈ comap Subtype.val (𝓝[Iio b] b)
obtain ⟨x : s, hx : ∀ z, x ≤ z → z ∈ u⟩ := mem_atTop_sets.1 hu
no goals
case intro.intro.a.mpr.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a✝ b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : Set.Nonempty s → ∃ a, a < b ∧ Ioo a b ⊆ s
✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
hu : u ∈ atTop
x : ↑s
hx : ∀ (z : ↑s), x ≤ z → z ∈ u
⊢ u ∈ comap Subtype.val (𝓝[Iio b] b)
exact ⟨Ioo x b, Ioo_mem_nhdsWithin_Iio' (hb x.2), fun z hz => hx _ hz.1.le⟩