α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
⊢ MeasurableSet s
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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 → ∃ y, x < y
⊢ MeasurableSet s
choose! M hM using h'
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
H : Set.Countable (s \ interior s)
⊢ MeasurableSet s

case H
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
⊢ Set.Countable (s \ interior s)
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
⊢ MeasurableSet s
suffices H : (s \ interior s).Countable
case H
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
A : ∀ (x : α), x ∈ s → ∃ y, y ∈ Ioi x ∧ Ioo x y ⊆ s
⊢ Set.Countable (s \ interior s)
case H
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
⊢ Set.Countable (s \ interior s)
have A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s := fun x hx =>
  (mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' (hM x hx)).1 (h x hx)
case H
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
⊢ Set.Countable (s \ interior s)
case H
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
A : ∀ (x : α), x ∈ s → ∃ y, y ∈ Ioi x ∧ Ioo x y ⊆ s
⊢ Set.Countable (s \ interior s)
choose! y hy h'y using A
no goals
case H
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
B : PairwiseDisjoint (s \ interior s) fun x => Ioo x (y x)
⊢ Set.Countable (s \ interior s)
exact B.countable_of_Ioo fun x hx => hy x hx.1
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
H : Set.Countable (s \ interior s)
this : s = interior s ∪ s \ interior s
⊢ MeasurableSet s
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
H : Set.Countable (s \ interior s)
⊢ MeasurableSet s
have : s = interior s ∪ s \ interior s := by rw [union_diff_cancel interior_subset]
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
H : Set.Countable (s \ interior s)
this : s = interior s ∪ s \ interior s
⊢ MeasurableSet (interior s ∪ s \ interior s)
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
H : Set.Countable (s \ interior s)
this : s = interior s ∪ s \ interior s
⊢ MeasurableSet s
rw [this]
no goals
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
H : Set.Countable (s \ interior s)
this : s = interior s ∪ s \ interior s
⊢ MeasurableSet (interior s ∪ s \ interior s)
exact isOpen_interior.measurableSet.union H.measurableSet
no goals
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
H : Set.Countable (s \ interior s)
⊢ s = interior s ∪ s \ interior s
rw [union_diff_cancel interior_subset]
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
⊢ (Disjoint on fun x => Ioo x (y x)) x x'
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
⊢ PairwiseDisjoint (s \ interior s) fun x => Ioo x (y x)
intro x hx x' hx' hxx'
case inl
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
⊢ (Disjoint on fun x => Ioo x (y x)) x x'

case inr
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x > x'
⊢ (Disjoint on fun x => Ioo x (y x)) x x'
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
⊢ (Disjoint on fun x => Ioo x (y x)) x x'
rcases lt_or_gt_of_ne hxx' with (h' | h')
case inl
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : z ∈ (fun x => Ioo x (y x)) x
h'z : z ∈ (fun x => Ioo x (y x)) x'
⊢ False
case inl
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
⊢ (Disjoint on fun x => Ioo x (y x)) x x'
refine disjoint_left.2 fun z hz h'z => ?_
case inl
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : z ∈ (fun x => Ioo x (y x)) x
h'z : z ∈ (fun x => Ioo x (y x)) x'
this : x' ∈ interior s
⊢ False
case inl
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : z ∈ (fun x => Ioo x (y x)) x
h'z : z ∈ (fun x => Ioo x (y x)) x'
⊢ False
have : x' ∈ interior s :=
  mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
no goals
case inl
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : z ∈ (fun x => Ioo x (y x)) x
h'z : z ∈ (fun x => Ioo x (y x)) x'
this : x' ∈ interior s
⊢ False
exact False.elim (hx'.2 this)
case inr
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x > x'
z : α
hz : z ∈ (fun x => Ioo x (y x)) x
h'z : z ∈ (fun x => Ioo x (y x)) x'
⊢ False
case inr
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x > x'
⊢ (Disjoint on fun x => Ioo x (y x)) x x'
refine disjoint_left.2 fun z hz h'z => ?_
case inr
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x > x'
z : α
hz : z ∈ (fun x => Ioo x (y x)) x
h'z : z ∈ (fun x => Ioo x (y x)) x'
this : x ∈ interior s
⊢ False
case inr
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x > x'
z : α
hz : z ∈ (fun x => Ioo x (y x)) x
h'z : z ∈ (fun x => Ioo x (y x)) x'
⊢ False
have : x ∈ interior s :=
  mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
no goals
case inr
α : Type u_1
β : Type ?u.1394071
γ : Type ?u.1394074
γ₂ : Type ?u.1394077
δ : Type ?u.1394080
ι : 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
M : α → α
hM : ∀ (x : α), x ∈ s → x < M x
y : α → α
hy : ∀ (x : α), x ∈ s → y x ∈ Ioi x
h'y : ∀ (x : α), x ∈ s → Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x > x'
z : α
hz : z ∈ (fun x => Ioo x (y x)) x
h'z : z ∈ (fun x => Ioo x (y x)) x'
this : x ∈ interior s
⊢ False
exact False.elim (hx.2 this)