α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
⊢ ContinuousWithinAt f (Ici a) a
refine' continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => _
case intro.intro.intro
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
rcases(mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
case intro.intro.intro
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
rcases exists_between hab' with ⟨c', hc'⟩
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
c : α
hcs : c ∈ s
hc : f c ∈ Ioo (f a) b'
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with
  ⟨_, hc, ⟨c, hcs, rfl⟩⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
c : α
hcs : c ∈ s
hc : f c ∈ Ioo (f a) b'
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
exact ⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩