case pos
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ∃ x, x ∈ s ∧ IsTop x
⊢ MeasurableSet s

case neg
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ¬∃ x, x ∈ s ∧ IsTop x
⊢ MeasurableSet s
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
⊢ MeasurableSet s
by_cases H : ∃ x ∈ s, IsTop x
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ MeasurableSet s
case pos
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ∃ x, x ∈ s ∧ IsTop x
⊢ MeasurableSet s
rcases H with ⟨x₀, x₀s, h₀⟩
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet s
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ MeasurableSet s
have : s = {x₀} ∪ s \ {x₀} := by rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet ({x₀} ∪ s \ {x₀})
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet s
rw [this]
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet (s \ {x₀})
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet ({x₀} ∪ s \ {x₀})
refine' (measurableSet_singleton _).union _
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ (x : α), x ∈ s \ {x₀} → x < x₀
⊢ MeasurableSet (s \ {x₀})
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet (s \ {x₀})
have A : ∀ x ∈ s \ {x₀}, x < x₀ := fun x hx => lt_of_le_of_ne (h₀ _) (by simpa using hx.2)
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ (x : α), x ∈ s \ {x₀} → x < x₀
x : α
hx : x ∈ s \ {x₀}
⊢ s \ {x₀} ∈ 𝓝[Ioi x] x
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ (x : α), x ∈ s \ {x₀} → x < x₀
⊢ MeasurableSet (s \ {x₀})
refine' measurableSet_of_mem_nhdsWithin_Ioi_aux (fun x hx => _) fun x hx => ⟨x₀, A x hx⟩
case pos.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u✝ : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ (x : α), x ∈ s \ {x₀} → x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
⊢ s \ {x₀} ∈ 𝓝[Ioi x] x
case pos.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ (x : α), x ∈ s \ {x₀} → x < x₀
x : α
hx : x ∈ s \ {x₀}
⊢ s \ {x₀} ∈ 𝓝[Ioi x] x
obtain ⟨u, hu, us⟩ : ∃ (u : α), u ∈ Ioi x ∧ Ioo x u ⊆ s :=
  (mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' (A x hx)).1 (h x hx.1)
case pos.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u✝ : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ (x : α), x ∈ s \ {x₀} → x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
y : α
hy : y ∈ Ioo x u
⊢ ¬y ∈ {x₀}
case pos.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u✝ : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ (x : α), x ∈ s \ {x₀} → x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
⊢ s \ {x₀} ∈ 𝓝[Ioi x] x
refine' (mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' (A x hx)).2 ⟨u, hu, fun y hy => ⟨us hy, _⟩⟩
no goals
case pos.intro.intro.intro.intro
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u✝ : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ (x : α), x ∈ s \ {x₀} → x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
y : α
hy : y ∈ Ioo x u
⊢ ¬y ∈ {x₀}
exact ne_of_lt (hy.2.trans_le (h₀ _))
no goals
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ s = {x₀} ∪ s \ {x₀}
rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]
no goals
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
x : α
hx : x ∈ s \ {x₀}
⊢ x ≠ x₀
simpa using hx.2
case neg
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ¬∃ x, x ∈ s ∧ IsTop x
⊢ ∀ (x : α), x ∈ s → ∃ y, x < y
case neg
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ¬∃ x, x ∈ s ∧ IsTop x
⊢ MeasurableSet s
apply measurableSet_of_mem_nhdsWithin_Ioi_aux h
case neg
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ¬∃ x, x ∈ s ∧ ∀ (b : α), b ≤ x
⊢ ∀ (x : α), x ∈ s → ∃ y, x < y
case neg
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ¬∃ x, x ∈ s ∧ IsTop x
⊢ ∀ (x : α), x ∈ s → ∃ y, x < y
simp only [IsTop] at H
case neg
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ∀ (x : α), x ∈ s → ∃ b, x < b
⊢ ∀ (x : α), x ∈ s → ∃ y, x < y
case neg
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ¬∃ x, x ∈ s ∧ ∀ (b : α), b ≤ x
⊢ ∀ (x : α), x ∈ s → ∃ y, x < y
push_neg  at H
no goals
case neg
α : Type u_1
β : Type ?u.1398323
γ : Type ?u.1398326
γ₂ : Type ?u.1398329
δ : Type ?u.1398332
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ (x : α), x ∈ s → s ∈ 𝓝[Ioi x] x
H : ∀ (x : α), x ∈ s → ∃ b, x < b
⊢ ∀ (x : α), x ∈ s → ∃ y, x < y
exact H